Algebraic specification[1] [2] [3] [4] is a software engineering technique for formally specifying system behavior. It was a very active subject of computer science research around 1980.[5]
Algebraic specification seeks to systematically develop more efficient programs by:
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:
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
(not not x)=x
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.