|The CoFI-Language Group Home Page|
Common Algebraic Specification LanguageThe CASL Summary version 1.0 can be obtained here:
Many-sorted basic specifications in CASL denote classes of many-sorted partial first-order structures: algebras where the functions are partial or total, and where also predicates are allowed. Axioms are first-order formulae built from equations and definedness assertions. Sort generation constraints can be stated. Datatype declarations are provided for concise specification of sorts together with some constructors and (optional) selectors. Subsorted basic specifications provide moreover a simple treatment of subsorts, interpreting subsort inclusion as embedding.
Structured specifications allow translation, reduction, union, and extension of specifications. Extensions may be required to be free; initiality constraints are a special case. A simple form of generic specifications is provided, together with instantiation involving parameter-fitting translations and views.
Architectural specifications express that the specified software is to be composed from separately-developed, reusable units with clear interfaces.
Finally, specification libraries allow the (distributed) storage and retrieval of named specifications.
This document gives a detailed summary of the syntax and intended
semantics of CASL. It is intended for readers who are already
familiar with the main concepts of algebraic specifications.