Go backward to 3.2 Semantic Concepts
Go up to 3 Basic Specifications
Go forward to 3.4 Example

3.3 Language Constructs

This section provides examples that illustrate the CASL language constructs for use in basic specifications: declarations and definitions (of sorts, operations, predicates, and datatypes), sort generation constraints, and axioms (involving variable declarations, quantifiers, connectives, atomic formulae, and terms). The examples are shown in display format; for input, a suggestive (ASCII or ISO Latin-1) plain text approximation is used, e.g., ` -> ' is input as `->', and `forall ' is input as `forall'.

Note that CASL allows declarations to be interspersed with definitions and axioms (as illustrated in Section 3.4). Visibility is linear: symbols have to be declared before they can be used (except within datatype declarations, where non-linear visibility allows mutually-recursive datatypes--e.g., List and NeList on page X).

Sorts:

Several sorts may be declared at once, possibly as subsorts of some other sort:2
sorts
Elem, List
sorts
Nat, Neg < Int
The values of a subsort may also be defined by a formula, e.g.:
sort
Pos = { n:Nat · n > 0 }
This corresponds to declaring Pos < Nat and asserting that a value n in Nat is the embedding of some value from Pos iff the formula n > 0 holds.

Operations:

Operations may be declared as total (using ` -> ') or partial (using ` ->? ') and given familiar attributes:
ops
0 : Nat ;
suc : Nat -> Nat ;
pre : Nat ->? Nat ;
__+__ : Nat × Nat -> Nat, assoc, comm, unit 0
So-called mixfix notation is allowed: place-holders for arguments are written as pairs of underscores (single underscores are treated as letters in identifiers). All symbols should be input in the ISO Latin-1 character set, but annotations3 may cause them to be displayed differently, e.g., as mathematical symbols.

In simple cases, operations may also be defined at the same time they are declared:

ops
1 : Nat = suc(0) ;
dbl(n:Nat) : Nat = n+n

Predicates:

Predicate declarations resemble operation declarations, but there is no result sort:
preds
odd : Nat ;
__<__ : Nat × Nat
They too may also be defined at the same time they are declared:
preds
even(n:Nat) <=> ¬ odd(n) ;
__ < __(m,n:Nat) <=> m<n \/ m=n

Datatypes:

A datatype declaration looks like a context-free grammar in a variant of BNF. It declares the symbols on the left of `::=' as sorts, and for each alternative on the right it declares a constructor--possibly with some selectors. When datatypes are declared as `free', the specified models are as for a free extension in a structured specification: distinct constructor terms of the same sort are interpreted as distinct values, and each declared sort is freely-generated by its constructors.
type
Collection ::= empty | just(Elem) | join(Collection; Collection)
free type
Bit ::= 0 | 1
free type
Pair ::= pair(left,right:Elem)
When there is more than one alternative in a datatype declaration, any selectors are generally partial and have to be declared as such, by inserting `?':4
free type
List ::= nil | cons(hd:?Elem; tl:?List)
Partial selectors can generally be avoided by use of subsort embeddings as constructors:
 
free types
List ::= nil | sort NeList;
NeList ::= cons(hd:Elem; tl:List)

The last declaration above illustrates non-linear visibility within a list of datatype declarations: NeList is used before it has been declared.

Sort Generation Constraints:

The CASL syntax allows datatypes to be declared as `generated', so that the sorts are constrained to be generated by their constructors (and embedded subsorts):
generated type
Bag ::= empty | add(Elem; Bag)
generated types
Nat ::= 0 | sort Pos;
Pos ::= suc(pre:Nat)
More generally, any group of signature declarations can be subject to a sort generation constraint, e.g.:
generated
{
sorts
Pos < Nat ;
ops
0 : Nat ;    suc : Nat -> Pos  }

Axioms:

Variables for use in axioms may be declared `globally', in advance:
vars
m,n : Nat; p : Pos
axioms
n < m => ...; suc(n)=p => ...; ...
Variables may also be declared locally to an `itemized' list of formulae:
vars
x, y, z : Elem
·
x < x
·
x < y /\ y < z => x < z
or within a formula using explicit quantification:
forall n:Nat · exists m:Nat · n < m
forall p:Pos · exists ! n:Nat · suc(n)=p
The logical connectives have their usual interpretation:
even(n) <=> ¬  odd(n)
m < n <=> m < n \/ m = n
m < n => ¬  n = 0
even(m+n) if odd(m) /\ odd(n)

Atomic Formulae:

Definedness assertions can be explicit:
defpre(suc(n)) /\ ¬ defpre(0)
or implicit in existential equations, which are distinguished from strong equations by writing ` =e= ' (input as `=e=') instead of `=':
defpre(n) => suc(pre(n)) =e= pre(suc(n))
¬ ok(x, e) => find(x, cons(e,l)) = find(x, l)
Subsort membership assertions are written suggestively using ` e ' (input as `in'):
n e Pos <=> defpre(n)
Applications of predicates are written the same way as those of operations, possibly using mixfix notation.

Terms:

Constants and variables may be written as sequences of words (optionally separated by single underscores--pairs of underscores are reserved for indicating place-holders in mixfix symbols--and decorated with primes) or mathematical signs: nil, empty_set, n, n', CURRENT_STATE.

Applications may be written using standard functional or mixfix notation: cons(e, l), {|e|} u s; they may also be written with explicit qualification, e.g., pre(n) may be written as (op pre:Nat ->? Nat)(n). Sorted terms (interpreted as applications of identity or subsort embeddings) are written straightforwardly, e.g.: dbl(suc(n):Nat). Casts (interpreted as applications of projections onto subsorts, the result of which may be undefined) are written using the reserved word `as', e.g.: pre(n as Pos).

CoFI Document: CASL/GuidedTour -- Version: 1 -- July 1999.
Comments to pdmosses@brics.dk

Go backward to 3.2 Semantic Concepts
Go up to 3 Basic Specifications
Go forward to 3.4 Example