CASL supports both partial and total algebraic specification. Partiality is a particularly natural and simple way of treating errors such as division by zero, and error propagation is implicit, so that whenever any argument of an operation is undefined, the result is undefined too. CASL also includes subsorts and error supersorts, to allow specification of exception handling when this is relevant. Totality is of course an important property, and CASL allows it to be declared along with the types of functions, rather than relegating it to the axioms. The domain of definition of a partial function may be made explicit by introducing it as a subsort of the argument sort and declaring the function to be total on it.
For instance, consider the familiar operations on (possibly-empty) lists: the list constructor cons would be declared as total, whereas the list head and tail selectors would be partial, being undefined on the empty list. The domain of definition of the selectors may be made explicit by introducing the subsort of non-empty lists, and declaring them to be total functions on that subsort. (This and further examples are specified in CASL in Section 3.3.)
In the presence of partiality, equations may require definedness: so-called `existential' equations require it, `strong' equations do not. In general, it is appropriate to use existential equations in conditions (since properties do not usually follow from undefinedness) but strong equations when defining partial functions inductively. So CASL allows both kinds of equations.
Definedness assertions can also be expressed directly. In fact definedness of a term is equivalent to its existential equality to itself--it could also be regarded as a unary predicate. Existential equality is equivalent to the conjunction of a strong equality and two definedness assertions; strong equality is equivalent to the conjunction of two conditionals involving only existential equality.
CASL is based on classical 2-valued first-order logic, with the standard interpretation of connectives. It supports user-declared predicates, which have some advantages over the (total) Boolean functions that were used instead of predicates in most previous languages.1 When an argument of a predicate is undefined, the predicate application cannot hold.
CASL provides the standard universal and existential quantification and logical connectives, i.e., ordinary first-order predicate logic. The motivation for this is expressiveness: restricting to conditional equations sometimes requires quite contrived specifications. For instance, it is a straightforward exercise to specify when a string is a permutation of another using quantifiers, and negation provides the complementary property; but the latter is quite awkward to specify using (positive) conditional equations.
The usual equational and conditional specification frameworks are provided as sublanguages of CASL, simply by restricting the use of quantifiers and logical connectives.
Most previous frameworks allow only one kind of model class to be specified. The default in CASL is to take all models of a specification, i.e., so-called loose semantics; but it is also possible to specify the restriction of models to the class of generated models (only expressible values are included, and properties may be proved by induction) or to the class of initial (and freely-generated) models (providing minimal satisfaction of atomic formulae). Of course initial models may not exist when disjunction, negation, etc., are used.
In a CASL specification the same symbol may be declared with various profiles (i.e., list of argument and result sorts), e.g. `+' may be declared as an operation on integers, reals, and strings. When such an overloaded symbol is used, the intended profile is to be determined by the context. Explicit disambiguation can be used when needed, by specifying the profile (or result sort) in an application.
It is appropriate to declare a sort as a subsort of another when the values of the subsort are regarded a special case of those in the other sort. For instance, the positive integers and the positive odd integers are best regarded as subsorts of the sort of natural numbers, which is itself a subsort of the integers. In contrast to most previous frameworks, CASL interprets subsorts as embeddings between carriers--not necessarily inclusions. This allows, e.g., models where values of sort integer are represented differently from values of sort real (as in most computers). CASL still allows the models where the subsort happens to be a subset. The extra generality of embeddings seems to be useful, and does not complicate the foundations at all.
Subsort embeddings commute with overloaded functions, so the values are independent of which profiles are used: 2+2=4, regardless of whether the `+' is that declared for natural numbers or integers.
CASL does not impose any conditions of `regularity', `coherence', or `sensibleness' on the relationship between overloading and subsorts. This is partly for simplicity (no such conditions are required for the semantics of CASL), partly because most such conditions lack modularity (which is a disadvantage in connection with structured specifications). Note that overloaded constants are allowed in CASL.
Specifications of `datatypes' with constructor and (possibly also) selector operations are frequently needed: they correspond to (unions of) record types and enumeration types in programming languages. CASL provides special constructs for datatype declarations to abbreviate the rather tedious declarations and axioms for constructors and selectors. Datatypes may be loose, generated, or free.