This section gives a concise overview of all the main CASL features, covering both that are in common with ASF+SDF as well as those that are not.
Basic specifications in CASL list declarations, definitions, and axioms.
Functions are partial or total, and predicates are allowed. Subsorts are interpreted as embeddings. Axioms are first-order formulae built from definedness assertions and both strong and existential equations. Sort generation constraints can be applied to groups of declarations. Datatype declarations are provided for concise specification of enumerations, unions, and products.
Structured specifications in CASL allow translation, reduction, union, and extension of specifications.
Extensions may be required to be conservative and/or free; initiality constraints are a special case. A simple form of generic specification is provided, together with instantiation involving parameter-fitting translations that affect compound identifiers.
Architectural specifications in CASL express implementation structure.
The specified software is to be composed from separately-developed, reusable units with clear interfaces.
Libraries in CASL provide collections of named specifications.
Downloading involves retrieval of specifications from distributed libraries.