User:Leland McInnes/Draft Algebraic Specification

Algebraic specification is a form of system specification that models systems using many sorted universal algebras.

Mathematics

Algebraic specification uses universal algebra over many-sorted sets. This acts as a form of typing. Given a set $S$ of sorts, an $S$-sorted set is a family of sets

$X=\langle X_{s}\rangle _{s\in S}$

of sets indexed by the elements of $S$. That is, X is a family of sets $X_{s}$ for each $s\in S$ such that all the elements of the set $X_{s}$ are "of sort $s\in S$". The usual set operations of union, intersection, disjoint union and cartesian product, as well as relations of inclusion and equality can be naturally extended to $S$-sorted sets.

We can define $S$-sorted $n$-ary operations on an $S$-sorted set, providing we define which sorts the operation acts on. We say a $S$-sorted operation

$f:s_{1}\times \cdots \times s_{n}\to s$

when the $i$th argument of $f$ must be of sort $s_{i}$ and the result sort must be $s$.

An $S$-sorted universal algebra is then a $S$-sorted set X, together with a set of $S$-sorted $n$-ary operations, where $n\geq 0$ and $n$ may be different for different operations.

Algebraic Specification Languages

• CASL and extensions.
• The Larch family of languages.
• OBJ3 and CafeOBJ