Book contents
Chapter 3 - Algebraic Specifications
Published online by Cambridge University Press: 19 January 2010
Summary
Algebraic specifications are used here for specifying standard notation for data, and for extending and specializing our standard notation for actions.
Our unorthodox framework for algebraic specification copes well with partial operations, generic data, polymorphism, and nondeterminism.
Algebraic specifications introduce symbols, assert axioms, and constrain models, as illustrated here by a natural example.
The grammars and semantic equations used in action semantic descriptions can easily be regarded as algebraic specifications.
The structural operational semantics of action notation is written as an algebraic specification of a transition function.
This chapter is mainly concerned with the details of how we specify notation for data. It also introduces the foundations of action semantics. Some readers may prefer to defer the detailed study of the example given here, because when reading action semantic descriptions one may take it for granted that data can indeed be specified algebraically, and that foundations do exist. Moreover, action notation does not depend much on the unorthodox features of our algebraic specification framework. On the other hand, readers who are used to conventional algebraic specifications are advised to look closely at this chapter before proceeding, as they may otherwise find it difficult to reconcile our examples with their experience.
First, some standard terminology. An algebra consists essentially of a universe, or carrier, of values, together with some distinguished operations on values. Operations of no arguments are called constants.
- Type
- Chapter
- Information
- Action Semantics , pp. 36 - 56Publisher: Cambridge University PressPrint publication year: 1992