Axiomatic and Algebraic Specification in Software Engineering

Axiomatic Specification

In the Axiomatic Specification of a system, first-order logic used to write the pre-and post-conditions to specify the operations of the system in the form of axioms. The pre-conditions capture the conditions that must be satisfied before an operation can successfully be invoked.

In essence, the pre-conditions capture the requirements on the input parameters of a function. The post-conditions are the conditions that must be satisfied when a function post-conditions are essentially constraints on the results produced for the function execution to be considered successful.

Algebraic Specification

In the Algebraic Specification technique, an object class or type is specified in terms of relationships existing between the operations defined on that type. It was first brought into prominence by Guttag (1980-1985) in the specification of abstract data types. Various notations of algebraic specifications have evolved, including those based on OBJ and Larch languages.

Essentially, algebraic specifications define a system as a heterogeneous algebra. A heterogeneous algebra is a collection of different sets on which several operations are defined. Traditional algebras are homogeneous. A
homogeneous algebra consists of a single set and several operations defined in this set such as – { +, -, *, / }.