Algebraic specification[1][2][3][4] is a software engineering technique for formally specifying system behavior.
[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.
In that case, an additional function true could be defined to yield the value not false, and an equation
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: 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.