Functions may be partial, the value of a function application in a term being possibly undefined. Total functions may be declared as such.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 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 language.
Signatures of CASL specifications distinguish between partial and total functions, the latter being required to be interpreted in all models as partial functions that happen to be totally-defined. It should be straightforward to define restricted languages that correspond to the conventional partial and total algebraic specification frameworks.
Atomic formulae expressing definedness are provided, 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. The design of 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.
Definedness of a term could be expressed by an existential equality, at the expense of writing the same term twice. It was deemed important to be able to express definedness of the value of a term directly by an atomic formula.
The underlying logic is 2-valued.Just because the values of terms may be undefined, one need not let this affect formulae (although various other frameworks have chosen to do so). In CASL, a (closed) formula is either satisfied or not, in any particular model. This keeps the interpretation of the logical connectives completely standard; the specifier may introduce particular three (or more) valued logics as and when required.