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. 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.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.
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.
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.
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.
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.
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.
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).
In CASL it is not possible to "base" generic specifications on other previously defined specifications. We think that this is a problematic design decision:
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:
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.
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.
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:
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.
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
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.
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.
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:
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.