The features of CASL that are missing from ASF+SDF include explicit treatment of partiality, general first-order axioms, some convenient abbreviations, and constructs for structuring specifications and implementations.
Adding some of these features to ASF+SDF (e.g., first-order axioms) would prohibit rapid-prototyping of specifications using term rewriting; others could probably be added without significant problems.
CASL allows partial functions.
Although total functions are an important special case of partial functions, the latter cannot be avoided in practical applications. CASL adopts the standard mathematical treatment of partiality: functions are `strict', with the undefinedness of any argument in an application forcing the undefinedness of the result. The lack of non-strict functions seems unproblematic in a pure specification framework, where undefinedness corresponds to the mere lack of a value, rather than to a computational notion of undefinedness. The specification of infinite values such as streams is not supported in CASL, although presumably it will be in some extension.
A partial function declaration is written (tentatively):
op f:S1×···×Sn -> ? SPartial constants can be declared too:
op c:? S
CASL provides atomic formulae expressing definedness, as well as both existential and strong equality.
When partial functions are used, the specifier should be careful to take account of the implications of axioms for definedness properties. Thus a clear distinction should be made between existential equality, where terms are asserted to have defined and equal values, and strong equality, where the terms may also both have undefined values. CASL includes both existential and strong equality, as each has its advantages: existential equality seems most natural to use in conditions of axioms (one does not usually want consequences to follow from the fact that two terms are both undefined), whereas strong equality seems `safer' to use in unconditional axioms, e.g., when specifying functions inductively.
Tentatively, a strong equation is written:
T1=T2and an existential equation as:
T1=!T2Definedness of a term is written:
T defined
CASL allows declarations of predicates.
It is quite common practice to eschew the use of predicates, taking (total) functions with results in some built-in sort of truth-values instead. As with restrictions to conditional equations, this may be convenient for prototyping, but it seems difficult to motivate at the level of using CASL for general specification and verification. Hence predicates may be declared in CASL, tentatively:
op p:pred(S1×···×Sn)
CASL allows definitions of subsorts, functions, and predicates.
Such definitions abbreviate commonly-occurring combinations of declarations and axioms. A subsort definition is written:
sort S={V:S' · F}and declares S to be the subsort of S' consisting of just those values of the variable V for which the formula F holds. A total function definition is written:
op f(V1:S1;...; Vn:Sn):S = Tand a constant definition as:
op c:S = TCASL also provides similar constructs for defining partial functions and predicates.
CASL allows axioms to be interspersed with declarations.
Why not?
CASL provides concise notation for declaring datatypes with constructors and (optional) selectors.
In a practical specification language, it is important to be able to avoid tedious, repetitive patterns of specification, as these are likely to be carelessly written, and never read closely. The CASL construct of a datatype declaration collects together several such cases into a single abbreviatory construct, which in some respects corresponds to a type definition in STANDARD ML, or to a context-free grammar production in BNF.
A datatype declaration is written (tentatively):
sort S>A1|···|AnIt declares a sort, and lists the alternatives A_i for that sort. An alternative may be a constant c, whose declaration is implicit; or it may be a list of sorts, written sorts S1,...,Sn, to be embedded as a subsort; or, finally, it may be a `construct'--essentially an indexed product--written f(...×fi:Si×...), given by a constructor function f together with its argument sorts S_i, each optionally accompanied by a selector f_i. The declarations of the constructors and selectors, and the assertion of the expected axioms that relate them to each other, are left implicit. When the > above is replaced by =, the specified sort is constrained to be generated by the specified constants, embedded subsorts, and constructor functions.
CASL allows all formulae of first-order logic.In fact many algebraic specification frameworks allow quantifiers and the usual logical connectives: the adjective `algebraic' refers to the specification of algebras, not to a possible restriction to purely equational specifications, which are algebraic in a different sense.
Universal quantification in CASL is written forall V:S · F. Existential quantification is written using exist , and exist 1 abbreviates a formula expressing existence of a unique value for which F holds.
The standard logical connectives are written F1 /\ F2, F1 \/ F2, F1 => F2 (alternatively F2 if F1), F1 <=> F2, and ¬F; the atomic formulae true and false are provided too.
CASL allows specification of both loose and initial classes of models.
In general, initial models of CASL specifications need not exist, due to the possibility of axioms involving disjunction and negation. When they do exist, the CASL construct for restricting the models of a specification SP to the initial ones:
freely SPcan be used, ensuring reachability--and also that atomic formulae (equations, definedness assertions, predicate applications) are as false as possible. The latter aspect is particularly convenient when specifying (e.g., transition) relations `inductively', as it would be tedious to have to specify all the cases when a relation is not to hold, as well as those where it should hold.
CASL allows specifications to be combined and extended, and extensions may be required to be free.For generality, CASL allows specifications with initial semantics to be united with those having loose semantics. This applies also to extensions: the specifications being extended may be either loose or free, and the extending part may be required to be a free extension, which is a natural generalization of the notion of initiality.
Union of specifications in CASL is written (tentatively):
SP_1 and...and SP_nand (ordinary) extension as:
enrich SP by SP'
CASL allows it to be specified that an extension is intended to be conservative.
The case where an extension is `conservative', not disturbing the models of the specifications being extended, occurs frequently. For example, when specifying a new function on numbers, one does not intend to change the models for numbers. Conservative extension in CASL is written:
enrich conservatively SP by SP'
CASL allows declared symbols to be translated and/or hidden.
Translation is needed primarily to allow the reuse of specifications with change of notation, which is important since different applications may require the use of different notation for the same entities. But also when specifications that have been developed in parallel are to be combined, some notational changes may be needed for consistency. Translation in CASL is written (tentatively):
SP renaming (...,SYi => SY'i, ...)
Hiding symbols ensures that they are not available to the user of the specification, which is appropriate for symbols that denote auxiliary entities, introduced by the specifier merely to facilitate the specification, and not necessarily to be implemented. CASL tentatively provides two constructs for hiding: one where the symbols to be hidden are listed directly (other symbols remaining visible--although hiding a sort entails hiding all function and predicate symbols whose profile involves that sort):
SP hiding (...,SYi, ...)the other where only the symbols to be `revealed' are listed:
SP revealing (...,SYi, ...)
In CASL the identical declaration of the same symbol in specifications that get combined is regarded as intentional.
Suppose that one unites two specifications that both declare the same symbol: the same sort, or functions or predicates with the same profiles. If this is regarded as well-formed (as it is in CASL) there are potentially (at least) two different interpretations: either the common symbol is regarded as shared, giving rise to a single symbol in the signature of the union, satisfying both the given specifications; or the two symbols are regarded as homonyms, i.e., different entities with the same name, which have somehow to be distinguished in the signature of the union.
CASL (following ASL and LARCH) takes the former interpretation, since the symbols declared by a specification (and not hidden) are assumed to denote entities of interest to the user, and unambiguous notation should be used for them. This treatment also has the advantage of semantic simplicity. However, due to the possibility of unintentional `clashes' between accidentally-left-unhidden auxiliary symbols, it is envisaged that CASL tools will be able to warn users about such cases. Note that when the two declarations of the symbol arise from the same original specification via separate extensions that later get united, the CASL interpretation gives the intended semantics, and moreover in such cases no warnings need be generated by tools.
CASL allows generic specifications, with instantiation affecting compound identifiers.
The parameters SP_i of a generic specification, which is written:
spec N[...,SP_i,...] = SPare simply dummy parts of the specification (declarations of symbols, axioms) that are intended to be replaced systematically whenever the name N of the generic specification is referred to in an instantiation, which is written:
N[...,SP'_i,...] where (...,SYj => SY'j,...)
The classic example is the generic specification of lists of arbitrary items: the parameter specification merely declares the sort of items, which gets replaced by particular sorts (e.g., of integers, characters) when instantiated. For a generic specification of ordered lists, the parameter specification would also declare a binary relation on items, and perhaps insist that it have (at least) the properties of a partial order.
It is possible to view generic specifications as a particular kind of loose specification, with instantiation having the effect of tightening up the specification. Thus generic lists of items are simply lists where the items have been left (extremely) loosely specified. Instantiating items to integers then amounts to translating the entire specification of lists accordingly (so that e.g. the first argument of the `cons' function is now declared to be an integer rather than an item) and forming its union with the specification of integers--the CASL treatment of common symbols in unions dealing correctly with the two declarations of the sort of integers.
CASL allows the use of compound identifiers for symbols in generic specifications.
The observant reader may have noticed that in the example described above, two different instantiations of the generic lists (say, for integers and characters) would declare the same sort symbol for the two different types of lists, causing problems when these get united. CASL allows the use of compound sort identifiers of the form:
SY[...,SY_i,...]in generic specifications; e.g., the sort of lists may be a symbol formed with the sort of items as a component, say List[Elem]. The translation of the parameter sort to the argument sort affects this compound sort symbol for lists too, giving distinct symbols such as List[Int], List[Char]for lists of integers and lists of characters, and thereby avoiding the danger of unintended identifications and the need for explicit renaming when combining instantiations.
CASL provides architectural specifications, for specifying the structure of models (which is generally not affected by the structure of the specification).The structuring constructs considered above allow a large specification to be presented in small, logically-organized parts, with the pragmatic benefits of comprehensibility and reusability. In CASL, the use of these constructs has absolutely no consequences for the structure of models, i.e., of the code that implements the specification. For instance, one may specify integers as an extension of natural numbers, or specify both together in a single basic specification; the models are the same.
It is especially important to bear this in mind in connection with generic specifications. The definition of a generic specification of lists of arbitrary items, and its instantiation on integers, does not imply that the implementation has to provide a parametrized program module for generic lists: all that is required is to provide lists of integers (although the implementor is free to choose to use a parametrized module, of course). Sannella, Sokolowski, and Tarlecki [SST92] provide extensive further discussion of these issues.
In contrast, an architectural specification requires that any model should consist of a collection of separate component units that can be composed in a particular way to give a resulting unit. Each component unit is to be implemented separately, providing a decomposition of the implementation task into separate subtasks with clear interfaces.
In CASL, an architectural specification consists of a collection of component unit specifications, together with a description of how the implemented units are to be composed. A model of such a specification consists of a model for each component unit specification, and the described composition.
CASL allows libraries to be distributed across sites on the Internet.An ordered collection of named specifications forms a library in CASL. Linear visibility is assumed: a specification in a library may refer only to the specifications that precede it.
Libraries may be located at particular sites on the Internet, and their current contents referenced by means of URL's.Given that there will be more than one CASL library of specifications (at least one library per project, plus one or more libraries of standard CASL specifications) the issue of how to refer from one library to another arises. The standard WWW notion of a Uniform Resource Locator (URL) seems well-suited for this purpose: a library may be identified with some index file located in a particular directory at a particular site, accessible by some specified protocol (e.g., FTP).
A library may require the `down-loading' of particular named specifications from other libraries each time it is used.Rather than allowing individual references to names throughout specifications to include the URLs of the relevant libraries (which might be inconvenient to maintain when libraries get reorganized), CASL provides a separate construct for down-loading named specifications from another library. Optionally, the specification may be given a local name different from its original name, so that one may easily avoid name clashes; the resemblance of this construct to the familiar FTP command `get' is intentional.