The Data Algebra
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 data algebra.

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