2 ASF+SDF n CASL

ASF+SDF and CASL have a significant number of features in common.

Here we consider the intersection of ASF+SDF and CASL: those concepts and constructs that are common to both languages. For each such ASF+SDF construct, we see how it might be expressed in CASL, using a tentative concrete syntax.

Both frameworks support the basic notions of many-sorted algebra with total functions.

A specification determines a signature (which gives the declared sorts and operation symbols, the latter coming together with the specified argument and result sorts) and the class of those models over the signature that satisfy the specified properties. Each model provides an algebra, i.e., a carrier set for each sort, and a function between carrier sets for each operation symbol.

ASF+SDF and CASL both allow arbitrary overloading, where the same operation symbol can declared with different argument and/or result sorts in the same specification.

In CASL the declaration of sorts S₁,...,S_n is written:

sorts S₁,...,S_n

op f:S₁×···×S_n -> S

op c: S

ASF+SDF and CASL both allow implicit injections from subsorts.

In CASL the declaration of a subsort S of a sort S' is written:

sort S < S'

ASF+SDF and CASL both allow infix, prefix, postfix, and general mixfix notation, as well as the conventional notation for function application.

In CASL the notation to be used for application is indicated by the use of placeholders `__' in the declared function symbol. E.g., infix notation for applying `+' is specified by declaring the symbol __+__ . If no place-holders are given, the conventional notation f(x,y,z) is used (omitting the parentheses when applying a constant c).

ASF+SDF and CASL both allow the declarations of sorts, operations, and variables to occur in any order.

In CASL the scope of declarations of sorts, operations, and variables is the entire enclosing list of such items. The declarations are written separated by semicolons, and the keywords introducing subsequent declarations of the same kind may be omitted:

sorts	S;
	S1< S;
ops	f:S1×···×Sn -> S;
	g:S1×···×Sn -> S

ASF+SDF and CASL both allow declarations of sorts and operations to be hidden.

In CASL the hiding of sort and operation symbols declared in a specification SP₁ and used in SP₂ is written (tentatively):

local SP_1 in SP_2

ASF+SDF and CASL both allow declarations of hidden variables.

In CASL variables are implicitly hidden, their scope always being the enclosing list of declarations and assertions. The declaration of variables V₁,...,V_n of sort S is written:

vars V_1,...,V_n: S

ASF+SDF and CASL both allow it to be specified which functions are constructors.

In CASL the constructors (i.e., generators) for some sorts are indicated by grouping them all together in a so-called sort generation constraint:

generated sorts ...; ops ... end

ASF+SDF and CASL both allow conditional equations and inequations as axioms.

In CASL conditional equations between terms T,T',T_i,T_i' are written:

T₁=T₁' /\ ... /\ T_n=T'_n => T=T'

T=T' if T₁=T₁' /\ ... /\ T_n=T'_n

¬ T=T'

ASF+SDF and CASL both allow specifications to be named and reused.

In CASL a specification named N extending specifications named N₁,...,N_m (corresponding to a module with imports in ASF+SDF) is written (tentatively):

spec N = enrich N_1,...,N_m by SP

ASF+SDF and CASL both allow informal comments, and the labelling of individual axioms.

In CASL the concrete syntax for comments and labels has not yet been decided, but it seems likely that end-of-line comments will start with `%%', and that labels will be written `%[...]'.

ASF+SDF and CASL both support formatting of specifications using mathematical symbols.

In CASL a declared symbol is displayed exactly as input in plain text (ISO Latin-1 character set) unless an explicit display annotation has been given for it. The concrete syntax for display annotations has not yet been decided, but it is expected to allow specification of separate display formats for plain text, LaTeX, HTML, and RTF.