Peter,There is a lot of experience in the RAISE group on how to design a specification language. Two things in particular:
I am also confused (but perhaps this is clear to those already involved) as to what CFI is *for*. It could be
- the division in the RAISE project between a group looking at method and a group looking at the language caused (almost) endless arguments. In particular the arguments for regularity and minimal concepts came from the method group; those for "the language should provide more guidance in what is sensible to write" came from the language group. The requirements for "separate development" (in particular the requirement for replacement of an abstract specification by an implementation of it to be possible and give you implementation of the context) caused a lot of problems because it ruled out simple VDM reification. CFI has a language group and a method group (though with some common membership). Why isn't there a requirements group?
- There are two possible views (at least!) on how to write semantics of a specification language: denotational and algebraic. My view is that users should be taught to see a specification in terms of its properties - what you can deduce from it - and that an algebraic semantics, a set of proof rules, is the most convenient. This is not completely an either/or question: one might have a denotational semantics as the "official" one and a set of proof rules shown to be consequences of it. But if you accept the primacy of proof rules to the users then it is the proof rules that should be most "clean" even if the denotations are complicated. This distinction also comes out in the approach to refinement. Peter's message refers to the chapter on Specification Languages (by Don Sannella and Martin Wirsing) from the forthcoming IFIP State-of-the-Art Report. I have read this and it generally seems to me a good discussion. Yet it does not mention the idea of refinement being defined proof-theoretically (as in RSL) rather than model-theoretically. It does mention the point that the use of observational abstraction makes refinement easy to define in terms of model class inclusion but the task of proving properties hard.
Peter Mosses' note suggests both of these at once in saying the problem is proliferation and this "hinders the dissemination and application of research results" and "[makes] it difficult to exploit standard examples, case studies and training material".
- a common framework for researchers to use as a basis, making it easier to evaluate and compare new ideas, or
- a language designed to be easy for practical use, embodying ideas generally thought to be useful and sound but separating these from the untried ideas currently subjects of research. Such a language, if commonly agreed on, would also encourage tool builders.
Regards,
Chris