including Referee Report on CASL
Handwritten/Typed Version, Tarquinia/Berlin, 6/11 June 1997
by
Hartmut Ehrig (Coordinator), José Meseguer, Ugo Montanari,
Fernando Orejas, Peter Padawitz, Francesco Parisi-Presicce,
Martin Wirsing, Uwe Wolter
This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.
This referee report is based on the presentation of CASL (Common Algebraic Specification Language) within CoFI (Common Framework Initiative) at the IFIP WG 1.3 Meeting on June 2 and 3, 1997, in Tarquinia.Response:
The response from the CASL designers has been inserted in the referee report, for ease of reference.The presentation of CASL included the rationale, language design features concerning Basic, Structural and Architectural Specifications, and Libraries, abstract and concrete syntax and a brief overview of main parts of the semantics. For most of these aspects carefully written papers were available already before the meeting, especially the rationale of CASL, or were presented during the meeting e.g. the incomplete draft semantics paper.
Response:
The Semantics task group has now completed the semantic description of the proposed language [Sem97].During the discussion at the IFIP Meeting it was suggested that a group of referees should be built up in order to provide an official IFIP WG 1.3 referee report. This report should be presented as quick as possible, preferably within the same week during the ADT Workshop, in order to allow a feedback between the referees and the authors of CASL. Unfortunately most of the referees were not able to read the rationale of CASL resp. other CASL papers before the meeting. Hence it was agreed that the referee report should be mainly based on the presentations and discussions during the IFIP meeting in order to avoid a time delay which would have been necessary to study all the CASL papers in sufficient detail.
Response:
The Language Design Task Group (abbreviated to "the designers" below) had indeed hoped that all the IFIP WG 1.3 members attending the meeting would have been able to read at least the CASL Rationale [LD97a] and Language Summary [LD97b] before the meeting, despite the heavy load of other commitments. The designers regret that they did not ascertain who had (not) read which documents in advance, as they might then have been able to focus more on larger conceptual issues during the presentation, rather than on the details of the choice of language constructs. For instance, the presentation of architectural specifications was very brief, and completely inadequate for those who had not read the rationale.Nevertheless, the designers agree that a prompt referee report on the basis of the CASL presentation was preferable to the delay that would have been necessary for detailed study of all the CASL documents. Their response to the referees' comments below includes references to particular sections of the Rationale and Language Summary, in case further discussion of these points is needed.
The general aim of CoFI and CASL to present a common algebraic specification language with methodology and tool support, which includes the best of all the existing algebraic specification languages is strongly supported by the referees. In the opinion of the referees the resulting language must be expressive and simple enough such that it is not only competitive with other existing algebraic and non-algebraic specification languages, but also superior with respect to specific aspects. The referees are aware that it is a very difficult but important task to achieve this aim, because there is a considerable diversity of different algebraic approaches and languages with important theoretical and practical results which have been developed within the last two decades by a wide spread algebraic specification community. Taking into account these difficulties the authors of CoFI and CASL have done an excellent job which is a very good basis to achieve the aims mentioned above. For this reason the referees support the tentative approval of CASL and recommend a revision according to the following general guidelines and specific recommendations.
Response:
The designers are grateful for the encouraging comments made by the referees. Some of them discussed already in Tarquinia the proposed guidelines and specific recommendations made by the referees; their response is detailed below.
The referees are convinced that the following three general guidelines are important for the success of CASL, but have not been reflected sufficiently in the present version:
Since the language is based on first order predicate logic, which is usually not considered to be algebraic, the algebraic flavor must be visible and convincing concerning other aspects. One of the main advantages of the algebraic approach is certainly the possibility of institution independence and structuring techniques which are based on categorical constructs in arbitrary institutions with suitable properties. This is an excellent opportunity to design a modular language where the structuring part is institution independent in order to accommodate several important underlying institutions. This idea seems not to be exploited well enough in the current version of CASL.
Response:
The designers will consider adjusting the design of CASL with a view to obtaining full institution-independence of the structuring part; currently, the presence of compound identifiers gives rise to some dependence.
In contrast to other specification techniques and languages for common software systems, like VDM and Z, there exists a large body of theoretical results for algebraic techniques and languages with strong practical impact for problems of consistency, correctness, compatibility and reusability in the software development process. The referees acknowledge the work and effort of the language designers to provide a specification framework where most of these theoretical results are still available and can be used with advantage in the software development process. In the present version of CASL, however, this is not enough visible.
Response:
The designers agree that the institutional structure should be more emphasized, and that the main properties of the underlying institution should be stated. This has already been included in the completed semantics for the proposed language [Sem97].
It is the intention of CASL to include most of the algebraic specification languages, which are well-established at least in the algebraic specification community, as sublanguages or extensions of CASL. Presently it is not sufficiently clear whether and how this be achieved in a convincing way, especially concerning the languages based on initial algebra semantics.
Response:
The authors agree that investigating the embedding of major existing specification languages--especially those based on initial semantics--in CASL is an important and urgent task. Their primary aim, however, is to be able to translate practical, existing specifications into CASL, and they question the necessity of embedding also "pathological cases" that are never used in practice.Unfortunately, CoFI does not currently have adequate resources for defining embeddings of existing languages into CASL, and has to rely on help with this task from those who are involved with the existing languages--at least to the extent of the reporting of any major difficulties that would probably arise when attempting such an embedding.
In CASL it is considered that the set of models of a given specification includes only algebras with non-empty carriers. This causes some (small) problems in relating CASL with a number of well-established specification languages (e.g. Clear, OBJ, ACT ONE) where this restriction is not considered. We are aware that this difference is not fundamental since it is significant only in cases where initial semantics is considered and the given specification includes empty sorts, which can hardly occur in practical cases (when loose semantics is considered there is a technical difference in the class of models, but logical consequence seems to be the same for formulas not including free variables). However, we do not see the need for this condition. On one hand it is true that, for total specifications, the proposed semantics makes deductive tools simpler. But, when considering partial functions with existential equality, the complications added by allowing models with empty carriers are subsumed by the complications of dealing with partiality. On the other hand, this condition adds some complication to the basic underlying theory. For instance, it is clear that one cannot expect a CASL specification to have initial semantics (independently of allowing empty carriers or not), but with the "non-empty carriers" condition one cannot expect having initial models in the equational restriction of CASL.
Response:
The current decision to exclude models with empty carriers is motivated by the interaction of this feature with variable declarations and implicit quantification, cf. Sect. 3.4 of the CASL Rationale [LD97a]. Moreover, the designers have been unable to find practical examples of specifications where models with empty carriers would be of any interest. Assuming that a change here would have only minor impact on the rest of the CASL design, the designers will reconsider this point, and would like to encourage the referees to provide any relevant practical examples involving models with empty carriers that are known to them.
In CASL both existential and strong equations are expressible. In our opinion, this may be a source of confusion for the user. However, we understand that there are situations where using one or the other equality may be more convenient. We think that the way of solving this problem is a matter of the presentation of the language. In particular, we think that in the language report one of the equalities (in particular, the existential one because of the better algebraic "behaviour") should be considered as basic, while the other one should be presented as a derived predicate (as a shorthand) indicating the situation where its use is recommended. In this sense, it may be a good idea to make an explicit distinction between the constructions of the language that are "basic" from the constructions that can be seen as syntactic sugar, i.e. to explicitly define what is the kernel sublanguage of CASL (see 3.1.5).
Response:
The designers agree that it may be helpful to indicate how some CASL constructs may be expressed in terms of others--but not that one should distinguish some particular kernel of CASL in the Language Summary.Concerning existential and strong equality (see also Sect. 3.1 of the CASL Rationale [LD97a]):
- Note that strong equality cannot be merely a derived predicate, since predicates never hold on undefined arguments.
- The desired algebraic properties of conditional specifications can be ensured by restricting the use of strong equality to conclusions. This could be enforced in a Horn clause sublanguage of CASL, but such a restriction seems useless in CASL with full first-order logic.
In the completed semantics [Sem97] (although not in the draft handed out in Tarquinia) existential equality is considered as basic with strong equality as an abbreviation. Similarly, implication is the only basic connective with conjunction, disjunction, negation, and equivalence as abbreviations.
Giving the semantics of CASL via definition of a kernel sub-language is not a bad idea. But the semantics task group didn't start that way so adopting this approach would be considerable extra work that it cannot afford now.
In CASL it is not possible to "base" generic specifications on other previously defined specifications. We think that this is a problematic design decision:
Response:
See the response to 3.3.2 below.
In CASL morphisms are 2nd class citizens, they can only be declared in some very specific contexts (e.g. within rename or derive declarations) and they cannot be named. We think that this is a bad design decision for several reasons:
Response:
The designers have asked those among them who most strongly favour allowing morphisms as first-class citizens to make a proposal for integrating these smoothly in the next version of CASL (see Note [Ber97]).
In the presentation of CASL's basic level, it was not completely clear what elements of the basic language are indeed basic and what can be seen as "syntactic sugar" which may be certainly useful for practical purposes. In particular, a naive impression could be that the CASL underlying institution is some kind of combination of 3 institutions: Partial first order logic with existential equality, partial first order logic with strong equality, and (a variety of) order-sorted first order logic.
Altogether, such a combination could be seen as too complex for the development of its basic theory. In this sense, we think that the explicit identification of the "Kernel Sublanguage" of CASL's basic level (for instance, partial first-order logic with existential equality), in terms of which the rest of basic features can be expressed would be of great help for the development of basic theory around CASL, for the design of deductive tools and for establishing relationships with existing institutions in algebraic specification languages.
Response:
See the response to 3.1.2 above.
We would recommend that some effort is devoted to making explicit within CASL different frequently used sublogics as sublanguages, together with, if possible, some detailed comments about how using such sublogics / sublanguages:
For example, clarifying the relationships with the logics of languages such as ACT 1 (many-sorted equational logic), OBJ3 (order-sorted equational logic), Maude (membership equational logic), and with Reichel's HEP specifications, as well as with other equational specification languages would be quite useful both to make even more clear the generality of CASL as well as for paving future work on reuse of existing systems to provide CASL with good tool support.
Response:
CASL has been designed with the aim of making it easy to cut down to different sublogics. For instance, removing partial function declarations (together with the `cast' construct, also partial selector functions in datatype declarations) gives a version of total subsorted logic; removing also declarations of subsorts and predicates gives ordinary many-sorted logic. Similarly, sublogics can be obtained by restricting the formulae allowed in axioms. But the designers agree that this should have been emphasized more in the CASL documents and presentation. The embedding of various existing algebraic specification languages (see 2.3 above) should also contribute to the identification of useful sublogics of CASL.
The CASL semantics is given in a natural semantics style based on a model-theoretic semantics of the resulting "value specifications". A "natural semantics" style is currently best practise for programming language semantics and seems certainly to be appropriate for static semantics and as a basis for the construction of various tools. In addition to the "natural style semantics" provided for CASL in the present version the referees suggest to present a language independent definition of the CASL-institutions and to exploit properties of these institutions in order to meet also the following requirements:
Response:
Language-independent definitions of the CASL institutions for many-sorted and subsorted specifications are sketched in the CASL Summary, and given in complete detail in the draft CASL Semantics. However, the designers agree that the important properties of these institutions should be stated and proved, and exploited explicitly where possible in the semantic definition of CASL constructs.The designers are unsure about exactly what kind of "structural properties of CASL semantics" the referees have in mind--some examples or further explanation would be helpful.
A further point of concern is the matter of the semantic definitions for the structural and architectural level. There is a well-developed body of concepts to give semantics to specification composition operations in a categorical and logic-independent way. This would be a big asset for CASL and would embody the best of the algebraic tradition. We have not seen this approach systematically followed in the presentations that were given. In particular, it would seem highly desirable to explain the architecture composition constructs precisely in these terms, using well-known theory composition concepts in a logic-independent way.
Response:
The designers will try to clarify the categorical features of the given semantics of the composition operators in a future version. Note, however, that architectural composition is merely composition of functions from algebras to algebras, and any connection to theory-composition concepts would be quite indirect. It would appear more relevant to state the relationship between the model-theoretic semantics and theory composition for the specification structuring constructs; this is quite standard, but should indeed be mentioned in the CASL documents.
In emphasizing the above points some referees suggest to develop an additional more abstract level of semantics for the structuring constructs of CASL. The abstract syntax could be given as a (meta-)signature with a minimal and orthogonal set of specification-building constructors representing the structuring concepts of CASL. The semantics of these constructors should be given in a compositional (institution-independent) way. This should simplify the static as well as the model semantics and should lead to a more abstract presentation of the semantics which would then be at a similar level of abstraction as the description given in the informal CASL Rationale. As a consequence such a semantics could close the gap between the rationale and the current semantics description. For instance, a simplified version of the extension construct might read syntactically as follows:
EXTENSION ::= extension | cons-ext SPEC SPEC SPEC ::= free-spec SPEC | local-spec SPEC SPEC
Response:
The designers agree that such a cut-down syntax and semantics might make a useful addition to the current CASL documents, and allow readers to get the main points of the language design and semantics without having to deal with all the lesser details. Unfortunately, it is unlikely that the designers will be able to find resources for this additional level of semantics without a funded project. The next version of the CASL Summary should, however, provide a more compact form of the abstract syntax grammar, with all superfluous nonterminals eliminated.
There should be a clear policy, that should be explained in the language report, to decide when a specification is ill-formed and, as a consequence, it has no semantics or when is perfectly "legal" but it is inconsistent.
Response:
The designers agree with this recommendation of the referees, and will change the CASL Summary and Semantics accordingly, cf. Note of Dissent L-5 [Bau97].
From the presentations and discussions in the IFIP WG meeting it was not possible for several of us to either fully understand all the subtleties involved, or to see why it was so important to keep such a strict separation between generic specifications on the one hand and functional module expressions used in architectural descriptions on the other.
In spite of not fully understanding the details, our shared perception is that there may be too many mechanisms to achieve quite similar ends, or in any case that a more unified treatment of generics and architectural functional expressions would make the language simpler and easier to understand.
Response:
The designers agree that the methodological motivations for the distinction between generic and architectural specifications should be explained more carefully. The conceptual and semantic differences are, however, explicitly addressed in both the CASL Rationale [LD97a] and Summary [LD97b]; see also [SST92]. Moreover, the structuring and architectural levels of CASL are essentially independent, and those users who do not themselves need to express architectural design decisions (with the accompanying isolation of development subtasks with clear interfaces) are not affected at all by the constructs provided for this in CASL.
In CASL actualization of generic specifications is done by means of an "almost" pushout, i.e. it is a pushout only when the shared symbols of the body and actual parameter specifications are all included in the formal parameter specification. We think that this is a bad design decision for the following reasons:
Response:
The designers agree on the desirability of the semantics of instantiation being a pushout. However, in view of the need to explicitly control the names used in specifications and to keep the naming mechanism reasonable simple, this cannot be ensured in all the cases of all possible actual parameters and fitting morphisms. The designers will revise the abstract syntax and semantics of generic extensions and instantiation to practically remove the disturbing cases, e.g., by distinguishing the "fixed" part of parameters (already considered at an earlier stage of the design, but later regarded as superfluous and removed) or introducing "imported base specifications", and by imposing conditions on the fitting morphism such that the result indeed corresponds to a pushout whenever it is defined.
There are two competing proposals for the syntax of CASL, the "Bremen" and the "Paris" proposal. Both proposals emphazise the necessity of an input and a display syntax, but differ w.r.t. to the concrete syntax. The "Bremen" proposal has a Z-like look, whereas the "Paris" proposal follows the "classical" style of algebraic specification languages such as ACT ONE, PLUSS, Larch and OBJ. Concerning basic specifications the "Paris" proposal is keyword based whereas the "Bremen" proposal uses different symbols for indicating function and predicate types.
The referees acknowledge the design efforts and the detailed and well-thought considerations of both proposals. They suggest to base the detailed design of the concrete syntax on the "Paris" approach with the exception of the types of function symbols and predicate symbols where the "Bremen" approach is more appropriate. In this way it should be possible to obtain a concrete syntax which is similar to well-known algebraic specification languages and which leaves also room for extension as e.g. to higher-order functions.
Response:
Some participants of the Language Design task group are now working towards a compromise between the "Bremen" and "Paris" proposals for concrete syntax, taking into account the recommendations of the referees.
Response:
The final design documents for CASL will include an explanation of how the above responses are reflected in it.