The components of a system must use the same representations for the data values that they share, or else they will not be able to communicate. For this reason, it makes sense to have a fixed collection of data values, bundled together into a single fixed algebra D of data values, called the

Let V be the sort set of D, and let
be its signature. Elements of V are called
**visible sorts**,
and
is called the **visible signature**.

Effective verification of a system will require an effective specification of its data algebra. We will assume that the data algebra is specified by an OBJ "object;" this means we have initial algebra semantics, which also supports proofs by induction.

[Next] [Prev] [Home] [BHome]

11 October 1996