Algebraic specification

Algebraic specification is a software engineering technique for formally specifying system behavior. It was a very active subject of computer science research around 1980.

Overview

Algebraic specification seeks to systematically develop more efficient programs by:

1. formally defining types of data, and mathematical operations on those data types
2. abstracting implementation details, such as the size of representations (in memory) and the efficiency of obtaining outcome of computations
3. formalizing the computations and operations on data types
4. allowing for automation by formally restricting operations to this limited set of behaviors and data types.

An algebraic specification achieves these goals by defining one or more data types, and specifying a collection of functions that operate on those data types. These functions can be divided into two classes:

1. Constructor functions: Functions that create or initialize the data elements, or construct complex elements from simpler ones. The set of available constructor functions is implied by the specification's signature. Additionally, a specification can contain equations defining equivalences between the objects constructed by these functions. Whether the underlying representation is identical for different but equivalent constructions is implementation-dependent.
2. Additional functions: Functions that operate on the data types, and are defined in terms of the constructor functions.

Examples

Consider a formal algebraic specification for the boolean data type.

One possible algebraic specification may provide two constructor functions for the data-element: a true constructor and a false constructor. Thus, a boolean data element could be declared, constructed, and initialized to a value. In this scenario, all other connective elements, such as XOR and AND, would be additional functions. Thus, a data element could be instantiated with either "true" or "false" value, and additional functions could be used to perform any operation on the data element.

Alternatively, the entire system of boolean data types could be specified using a different set of constructor functions: a false constructor and a not constructor. In that case, an additional function true could be defined to yield the value not false, and an equation [math]\displaystyle{ (\text{not} \; \text{not} \; x) = x }[/math] should be added.

The algebraic specification therefore describes all possible states of the data element, and all possible transitions between states.

For a more complicated example, the integers can be specified (among many other ways, and choosing one of the many formalisms) with two constructors

  1 : Z
  (_ - _) : Z × Z -> Z

and three equations:

            (1 - (1 - p)) = p
      ((1 - (n - p)) - 1) = (p - n)
  ((p1 - n1) - (n2 - p2)) = (p1 - (n1 - (p2 - n2)))

It is easy to verify that the equations are valid, given the usual interpretation of the binary "minus" function. (The variable names have been chosen to hint at positive and negative contributions to the value.) With a little effort, it can be shown that, applied left to right, they also constitute a confluent and terminating rewriting system, mapping any constructed term to an unambiguous normal form representing the respective integer:

  ...
  (((1 - 1) - 1) - 1)
  ((1 - 1) - 1)
  (1 - 1)
  1
  (1 - ((1 - 1) - 1))
  (1 - (((1 - 1) - 1) - 1))
  ...

Therefore, any implementation conforming to this specification will behave like the integers, or possibly a restricted range of them, like the usual integer types found in most programming languages.

See also

• Common Algebraic Specification Language
• Formal specification
• OBJ