4.2 Algebraic Specifications

The classic example of algebraic specifications is the definition of a stack, which includes the axiom pop(put(s, x)) = s. Implicit definitions in forms of axioms stating the properties of the component free us from selecting a representation. Algebraic specifications have a number of appealing mathematical properties. Their practical use, however, is rather cumbersome. Operations are not specified individually. It is difficult to find a sufficient and minimal set of axioms for a given component. The forced style of thinking does not match well with the imperative paradigm, in which most programmers think and implement. External calls cannot be handled in a satisfactory manner. Thus, algebraic specifications do not meet the requirements for grey-box specifications.