The initial version of this document is still available. This document incorporates the entire original
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, and Uwe Wolter
This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.3.
This referee report is based on the presentation of CASL (Common Algebraic Specification Language) within CoFI (Common Framework Initiative) at the IFIP WG1.3 Meeting on June 2 and 3, 1997, in Tarquinia.Response:
The present document includes also the response the CASL designers to the referees.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 original CASL design proposal, submitted to IFIP WG1.3 on 14 May 1997 by the CASL Language Design Task Group and presented at its meeting in Tarquinia, consisted of the documents listed in [CoF97c]: the rationale for CoFI [CoF97a] and CASL [Mos97b], the CASL Language Summary (version 0.97) [CoF97e], a summary of the intended CASL tools [CoF97g], two proposals for concrete syntax for CASL, a draft formal semantics [CoF97f], and some notes of dissent addressing particular design decisions [CoF97d].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 WG1.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 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 submitted CASL documents. The initial response of the designers to the referee report was made in August 1997 [CoF97b]. The CASL design (version 1.0) was finalized in October 19981 [CoF98]; the present final response indicates how the various points raised by the referees are reflected in the final design of CASL v1.0.
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 were grateful for the encouraging comments made by the referees, and for the tentative approval of the proposed design for CASL. They have subsequently made considerable efforts to follow the recommendations and suggestions of the IFIP WG1.3 referees, and they believe that this has led to significant improvements in the CASL design. On some points, however, reconsideration of the design issues did not lead to following the specific recommendations and suggestions of the referees, as explained below; the designers hope that the referees find the given explanations satisfactory.The designers believe that there is a consensus that CASL is now fully appropriate as a Common Algebraic Specification Language, satisfying the stated aims and scope [Mos97b]. The referees' support for the final approval of CASL by IFIP WG1.3 is hereby requested.
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 flavour 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:
Although the original approaches to algebraic specification were based on equational logic for standard many-sorted algebras, numerous well-motivated modifications of the original purely algebraic paradigm have subsequently been proposed and used within the algebraic specification community. In the view of the CASL designers, the most essential aspect of the algebraic approaches is that software systems are modelled as algebraic structures of some kind. In this sense, CASL is certainly algebraic, despite its use of predicates, subsorts, first-order axioms, etc.The designers have adjusted the design of CASL so that a complete institution-independence of the structuring part is obtained. More precisely, the semantics of structured specifications is given for an arbitrary institution with qualified symbols, independently of the specific interpretation of the basic concepts in the underlying CASL institution. The extra structure on the institution (symbols, qualification) is needed to deal with symbol mappings in a convenient way. Practically all institutions of interest can be easily equipped with this extra structure in a natural way. See [Mos00a] for more detail.
As for the semantics of architectural specifications, an additional component to deal with sharing between models must be added to institutions--the appropriate concept of an "institution with qualified symbols and sharing" and the corresponding semantic description of architectural constructs is currently under development.
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 underlying theory and methodology of algebraic specifications and formal software development have been a guiding factor throughout the design of CASL. In many cases, preservation of the basic results in the area is obvious, even if not made explicit in the Language Summary itself (which is aimed at a broad readership, and does not assume familiarity with Category Theory). There are other documents where such relevant facts are stated explicitly. For instance, the designers agree that the institutional structure of CASL should be emphasized, as in the completed semantics for CASL v1.0 [CoF99]: the properties of the underlying institution, as well as of the concepts underlying the design of CASL, are stated there when needed.
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 designers agree that investigating the embedding of major existing specification languages--especially those based on initial semantics--in CASL is an important and urgent task. At the level of specification-in-the-small, the Larch Shared Language, ACT ONE, ASF+SDF, OBJ3 and HEP-theories have been examined [Mos00b]. The outcome was that apart from the rather pathological case of algebras with empty carriers (see also the response to 3.1.1 below) all of these languages can be translated to sublanguages of CASL. Moreover, the translation is always straightforward, with the exception of OBJ3's retracts; their (a bit more complex) translation to CASL is studied in [Mos00b], where also, for each language, the corresponding sublanguage of CASL is indicated. Initial algebra semantics can be obtained with the free construct in CASL.At the level of specification-in-the-large, a first informal look has been taken at LSL, ACT TWO, ASF+SDF, and OBJ3 [Mos98b]. Though not every structuring construct of these languages can be translated literally to CASL, it is always possible to find a circumscription in CASL.
Informal comparisons of CASL with ASF+SDF [Mos97a] and with CafeOBJ [Mos00c] have also been made.
CoFI does not currently have adequate resources for defining embeddings of more 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 decision to exclude models with empty carriers is motivated by the interaction of this feature with variable declarations and implicit quantification [CoF98, Sect. 2.2].Since the standard definitions of first-order and higher-order logic forbid empty carriers as well, there is a straightforward bridge from CASL to FOL- or HOL-based theorem proving tools (which usually assume non-empty carriers). Empty carriers would overduly complicate the use of such tools for CASL.
Moreover, the designers have been unable to find practical examples of specifications where models with empty carriers would be essential. When one really needs to model possibly-empty finite collections (like sets or graphs), they can be represented as elements in a particular algebra rather than as algebras themselves. This can be done with the usual methods of inductively defining datatypes consisting of finite objects. Examples can be found in the libraries of basic datatypes (sets, graphs, lists, bags, etc.). This representation has also the advantage that one can specify operations and predicates acting on the collections, which would not be possible when modeling the collections as algebras. In the case that one needs to model infinite collections, one has to use specification of von Neumann-Bernays-Gödel set theory that has been developed in CASL. It allows to talk about arbitrary sets, like in ZFC.
If one really needs it, it is also possible to model possibly-empty collections as algebras in CASL. The trick is mainly to add a new element to each sort, to fix the behaviour of operations and predicates on this element, and to ignore it explicitly in quantifications. Formally, this gives an institution representation of (subsorted, partial) first-order logic with empty carriers into (subsorted, partial) first-order logic without empty carriers, see [Mos00b].
Concerning theoretical results about empty carriers: while examining the translation of OBJ3 to CASL, it was found that the algebra injection semantics of retracts in OBJ3 forms an institution only if empty carriers are not allowed [Mos00b].
Concerning initial models (resp. free extensions) in the conditional equational sublanguage of CASL, they do exist when the specification (resp. the body specification) is strict, i.e. has a ground term for each sort. Of course, this does not exclude the use of non-strict specifications in CASL--for example, parameter specifications often are not strict. However, it will hardly ever be the case that one wants to have initial or free semantics for non-strict theories [Mos00b, Mos99].
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 sometimes be helpful to indicate how some CASL constructs may be expressed in terms of others. However, they do not regard it as appropriate to distinguish some particular kernel of CASL in the Language Summary (see the response to 3.1.5 below).Concerning existential and strong equality (see also Sect. 3.1 of the CASL Rationale [Mos97b]):
- 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 of CASL [CoF99] 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. Although convenient for defining the formal semantics of CASL, such choices of what to regard as basic are generally somewhat arbitrary. The present description of the two equalities in the Language Summary appears to be as simple and straightforward as possible.
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:
The designers have followed the above recommendation by adding an import declaration to generic specifications (and, similarly, to specifications of generic views, and of generic units in architectural specifications). Both the body of a generic specification and the actual parameter during instantiation may make references to names from the imported specification. From the semantics point of view, the import acts as an additional parameter to the generic specification, which is always instantiated by itself. This approach ensures that the instantiation of a generic specification is a pushout also in cases where the body and the actual parameter refer to the same specifications, these specifications being in the import.See also 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:
Following the above recommendation, several proposals for allowing morphisms as first-class citizens in CASL have been considered [Ber97]. The simplest of the proposals has been adopted, allowing views to be defined along with specifications in libraries, and allowing reference to named views in instantiations. It has also been made more convenient to define views, by allowing identity mappings (and other symbol mappings that are uniquely determined by the source and target specifications of the view) to be left implicit.The proposal has subsequently been extended by allowing named views to be generic: instantiations of a generic view give composition of the morphism defined by the view with other fitting morphisms. Generic views may also have imports, which are implicitly mapped by identity morphisms.
Thus CASL now provides a treatment of views as first-class citizens, as recommended by the referees, with some enhancements concerning genericity that provide uniformity with the rest of the CASL design. One could of course go much further in this direction, but the CASL designers consider that their final design provides a good balance between simplicity, expressive power, and convenience. If practical use of CASL shows the desirability of additional constructs concerning views, their inclusion in some future version of the language will be considered.
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:
Regarding the relationship between existential and strong equality, see the response given to 3.1.2 above. Having both equalities available for use in sentences does not lead to any significant complication in the given institution for basic specifications in CASL.Concerning many- and order-sortedness, the CASL Semantics defines both a many-sorted institution (which is used for specifications that do not involve the subsorting constructs) and a subsorted institution (which may be used also when subsorting constructs are involved), together with a reduction of the latter to the former. The given reduction may be regarded as identifying many-sorted first-order specifications as a kernel sublanguage of CASL's basic specifications, and has indeed been useful for the purposes suggested above. We have also made an effort to present order-sorted concepts and constructs as extensions of the many-sorted part of CASL in the Language Summary [CoF98].
However, the designers consider that it would be inappropriate for the Language Summary to present CASL as a kernel language together with some "syntactic sugar". The choice of kernel constructs would probably be somewhat arbitrary, and seem unmotivated. Moreover, the de-sugaring of a non-kernel construct may be of little help for understanding it (for instance, translating negation to implication) or disproportionately tedious (as with translating free datatype declarations into other declarations and axioms). See also the discussion of the non-minimality of CASL in [Mos97b].
Deductive tools for CASL have been developed by reducing CASL to simpler languages [Mos00b]. There is no need to identify a kernel language for this task.
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. This is explained in detail in [Mos00b], where also all of the above mentioned specification languages are related to sublanguages of CASL. Also, the translation of CASL to sublanguages in order to obtain tool support is addressed.
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:
Ad 1: Language-independent definitions of the CASL institutions for many-sorted and subsorted specifications are sketched in the Language Summary, and given in complete detail in the CASL semantics. Some properties of these institutions have been proven:The failure of amalgamation in the institution for subsorted specifications is perhaps the most surprising and worrying fact above. However, the institution for subsorted specifications is an institution with qualified symbols [Mos00a] and can be equipped with sharing information to check the existence of amalgamation when required, which is all that is needed to provide well-defined semantics for CASL as a whole, and its architectural constructs in particular.
- the category of CASL signatures is cocomplete [Mos98a],
- the CASL institution for many-sorted specifications has amalgamation (this is a folklore theorem [BW85, Tar86] which has been explicitly stated in [CGRW95, Mos00b]), while this fails in the institution for subsorted specifications,
- the CASL institution for many-sorted specifications (without generation constraints, and with signature morphisms injective on sorts) has the Craig interpolation property [Bor99], while this fails in general in the full CASL institution (with subsorts and generation constraints).
The (partial) failure of interpolation is perhaps less surprising (generation constraints provide only a very limited fragment of infinitary logic). How to cope with the ensuing problem of completeness for any compositional proof system for CASL specifications is a subject of ongoing research.
Ad 2: The semantics of the CASL constructs is compositional, and moreover, the semantics of the structuring constructs can be formulated in terms of the semantics of an ASL-like language [Mos00a], which allows application of the theory of ASL-like languages to CASL.
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 "same name, same thing" principle is pervasive in CASL. This philosophy differs from the Clear-like approach of combining specifications via colimits. However, a suitable restriction in the language ensures that of instantiations of generic specifications always yield a pushout [Mos00a].Concerning architectural composition, and more generally, architectural constructs of CASL: these are merely operators on algebras (CASL structures) and applications of functions between them, and any connection to theory-composition concepts would be quite indirect. However, it is possible to link these constructs to the constructs for CASL structured specifications, as implicitly suggested by the presentation in [BST99]. It is 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 (and will be included in future work on proof theory for CASL specifications).
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:
In response to the above suggestion, an abbreviated grammar for the CASL abstract syntax has been included in the Language Summary [CoF98, App. B]. It was obtained from the original grammar [CoF98, App. A] by eliminating non-terminal symbols (which does not affect the specified set of trees). For example. the original grammar for structured specifications in CASL v1.0 includes:which reduces to the following productions in the abbreviated grammar:SPEC ::= EXTENSION | FREE-SPEC | LOCAL-SPEC | ... EXTENSION ::= extension SPEC+ FREE-SPEC ::= free-spec SPEC LOCAL-SPEC ::= local-spec SPEC SPECHowever, the abbreviated grammar is still specified in BNF, without use of the inline alternative components/constructors of Extended BNF used in the example given by the referees.2SPEC ::= extension SPEC+ | free-spec SPEC | local-spec SPEC SPECThe compositional rules given in the formal semantics generally involve only the constructors of the abstract syntax, and do not mention redundant non-terminals such as EXTENSION. Thus the semantics is independent of which of the two grammars is used to define the abstract syntax. Without introducing a kernel sublanguage (which would necessitate a rather tedious definition of a translation from the full language to the kernel in the formal semantics--see also the response to 3.1.2 above) it is not possible to eliminate constructors from the abstract syntax. In any case, to match the level of "abstraction" of the CASL Rationale, the formal semantics would have to be based on the concrete syntax of CASL, rather than on the abstract syntax; such a change would require a significant amount of work, and also raise questions about the well-definedness of the semantics. In [Mos00a], however, a kernel language for CASL structured specifications and its semantics is defined, allowing an easier study of the semantics.
Finally, note that both grammars for the CASL abstract syntax could straightforwardly be expressed in CASL itself (using datatype declarations). Selectors could then be added; for the CASL specification corresponding to the unabbreviated grammar, they would always be declared as total (since the range of each constructor is an entire sort) whereas for the other one, they would generally be declared as partial.
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 semantics of CASL consists of two parts: a decidable static semantics, which serves to delineate the class of statically well-formed CASL specifications, and model-level semantics which then deals with well-formed CASL specifications only. The latter semantics for some of the specification constructs involves model-theoretic conditions necessary for the semantics to be defined--for instance, in an instantiation of a parameterized specification, each model of the actual parameter specifications must correspond to a model of the formal parameter part (via the fitting morphism). Such conditions give rise to proof obligations that the user (possibly with the help of support tools) is expected to discharge when building specifications. In case these conditions are not met (and hence the corresponding proof obligations cannot be discharged), the semantic meaning for such a specification is left undefined. In general, this is an undecidable property. Indeed, this is quite different from inconsistency of specifications--there are of course many well-formed specifications that have no model. These issues are quite clear, in our view, in the completed semantics of CASL v1.0 (cf. also [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 (or perhaps more accurately: structured) and architectural specifications should be explained more carefully. The conceptual and semantic differences are, however, explicitly addressed in both the CASL Rationale [Mos97b] and Language Summary [CoF98]; see also [SST92]. Since then, the underlying methodological motivation, concepts and technical details underlying the design of architectural specifications have been presented in full in [BST99]. Summarizing: structured specifications give a presentation of the requirements imposed on the system to be developed, without constraining its internal structure, while architectural specifications prescribe the (top-level) modular structure of the system.Architectural specifications correspond to what [GHW82] call "organizational specifications": they define the structure of a system by specifying its components and how they fit together.
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, this cannot be ensured in all the cases of all possible actual parameters and fitting morphisms. The designers have added imports to generic specifications (cf. the response to 3.1.3) to remove the most disturbing cases where the body of a generic specification and the actual parameter share names which are intended to be the same. These names can be now put in the import. A suitable restriction in the language ensures that instantiations of generic specifications always yield a pushout [Mos00a].In view of the need to explicitly control the names used in specifications and to keep the naming mechanism reasonably simple, the semantics of instantiation is undefined in those cases where the body and the actual parameter share names by accident. Given the possibility of using imports and a mechanism to induce renaming of compound identifiers by fitting morphisms, the cases seem quite rare (or pathological) and anyhow, they can easily be avoided by explicitly renaming the disturbing components of the actual parameters when instantiating.
There are two competing proposals for the syntax of CASL, the "Bremen" and the "Paris" proposal. Both proposals emphasize 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:
The authors of the competing proposals have followed the above recommendations in the final design of the CASL concrete syntax.