Lambda the Ultimate

I am inclined to call this a "formal method" because of the use of a high level semantics. Programming languages typically start with a syntax/semantics closely related to machine codes. By this argument Scheme and Prolog would also be high level semantics (ie formal methods). I think that this is a useful distinction because the software art must address both problems; efficient machine codes and clear, "correct" semantics. How to do both with only one "language" without complex refinement steps between the two seems to be a problem.

BTW: I hate the expression "formal methods", Formal methods are intended to supply semantics that is not expressed in the programming language. The issue is really semantics, not formality.

Where do you draw the line between a specification language and a programming language? Hank says that programming languages have to have a syntax/semantics that's "close to the machine", but that definition would seem to place a lot of the things we typically think of as PLs into the spec language category. In your particular case, what you've described in the paper feels like a modelling or spec language to me, because it seems to abstract from many of the details you'd need to provide to create a real system (although that may be an artifact of the length of the article). I guess for me the real test is whether you actually compile your models down to executable application code, or use them simply as executable models for system specification but produce the application code via some kind of manual or automatic refinement (rather than straight translation or imterpretation) to some other language.

As an aside, I'm curious: the notion that a protocol machine can refuse certain events leads to the possibility of deadlock when interacting with other protocol machines - do you presently attempt to detect possible deadlocks in your models? If not, you might consider translating the models into machine-readable CSP, and running them through Formal Systems' FDR2 refinement checker or some other CSP analysis tool. That would provide a quick and early check on the consistency of the composite behavior that has been specified by the composition of various protocol machines. Alternatively, you could perhaps capture standard design rules to avoid deadlock, such as those laid out in Jeremy Martin's thesis, within your modelscope tool so that users are prevented from even creating models that are capable of deadlocking.

Thanks for your comments, Hank and Allan.

The current use of the language is for behaviour model development, and there is currently no capability to generate a "real system". So at the moment it is a "modelling or spec language". However, there is no reason in principle (as far as I know) why real systems should not be generated.

It is possible to create a model that deadlocks. However, we do not use conventional CSP formalisms, as it is not suitable for systems that have any degree of data complexity. My concern would be that converting a protocol machine into a conventional CSP (algebraic) process would sometimes be hard and would generate enormous CSP definitions. We have the concept of derived states (like derived attributes) which would also make the translation hard.

I would add that, in practice, our machines tend to be simple (6 states is a big machine) and deadlock is easy to spot. ModelScope shows it up quite readily.

Thanks for the pointer to Jeremy Martin's work -- I'll have a look.