AXIOMATIC AND ALGEBRAIC SPECIFICATION

Read Time:9 Minute, 31 Second

AXIOMATIC SPECIFICATION

In axiomatic specification of a system, first-order logic is used to write the pre- and post- conditions to specify the operations of the system in the form of axioms.

The pre-conditions basically 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.

How to develop an axiomatic specifications ?

The following are the sequence of steps that can be followed to systematically develop the axiomatic specifications of a function:

Establish the range of input values over which the function should behave correctly. Establish the constraints on the input parameters as a predicate.
Specify a predicate defining the condition which must hold on the output of the function if it behaved properly.
Establish the changes made to the function’s input parameters after execution of the function. Pure mathematical functions do not change their input and therefore this type assertion is not necessary for pure functions.
Combine all of the above into pre- and post-conditions of the function.

Examples of how simple abstract data types can be algebraically specified.

Example-1

Specify the pre- and post-conditions of a function that takes a real number as argument and returns half the input value if the input is less than or equal to 100, or else returns double the value.

f (x : real) : real

pre : x ∈ R

post : {(x ≤ 100) ∧ (f (x) = x/2)} ∨ {(x > 100) ∧ (f (x) = 2 ∗ x)}

Example-2

Axiomatically specify a function named search which takes an integer array and an integer key value as its arguments and returns the index in the array where the key value is present.

search(X : intArray, key : integer) : integer

pre : ∃i ∈ [X f irst…X last], X [i] = key post : {(X [search(X, key)] = key) ∧ (X = X)}

Please note that we have followed the convention that if a function changes any of its input parameters, and if that parameter is named X , then we refer to it after the function completes execution as X ’.

One practical application of the axiomatic specification is in program documentation. Engineers developing code for a function specify the function by noting down the pre and post conditions of the function in the function header.

Another application of the axiomatic specifications is in proving program properties by composing the pre and post-conditions of a number of functions.

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.

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; e.g. { I, +, -, *, / }.

In contrast, alphabetic strings S together with operations of concatenation and length {S, I , con, len}, is not a homogeneous algebra, since the range of the length operation is the set of integers.

Each set of symbols in a heterogeneous algebra is called a sort of the algebra.

To define a heterogeneous algebra, besides defining the sorts, we need to specify the involved operations, their signatures, and their domains and ranges.

Using algebraic specification, we define the meaning of a set of interface procedures by using equations.

An algebraic specification is usually presented in four sections.

Types section:

In this section, the sorts (or the data types) being used are specified.

Exception section:

This section gives the names of the exceptional conditions that might occur when different operations are carried out.

These exception conditions are used in the later sections of an algebraic specification.

Syntax section:

This section defines the signatures of the interface procedures. The collection of sets that form input domain of an operator and the sort where the output is produced are called the signature of the operator. For example, PUSH takes a stack and an element as its input and returns a new stack that has been created.

Equations section:

This section gives a set of rewrite rules (or equations) defining the meaning of the interface procedures in terms of each other.

In general, this section is allowed to contain conditional expressions. By convention each equation is implicitly universally quantified over all possible values of the variables.

This means that the equation holds for all possible values of the variable. Names not mentioned in the syntax section such r or e are variables.

The first step in defining an algebraic specification is to identify the set of required operations.

After having identified the required operators, it is helpful to classify them as either basic constructor operators, extra constructor operators, basic inspector operators, or extra inspection operators.

The definition of these categories of operators is as follows:

Basic construction operators:

These operators are used to create or modify entities of a type. The basic construction operators are essential to generate all possible elements of the type being specified.

For example, ‘create’ and ‘append’ are basic construction operators in the below example.

Extra construction operators:

These are the construction operators other than the basic construction operators.

For example, the operator ‘remove’ in the below example is an extra construction operator, because even without using ‘remove’ it is possible to generate all values of the type being specified.

Basic inspection operators:

These operators evaluate attributes of a type without modifying them, e.g., eval, get, etc.

Let S be the set of operators whose range is not the data type being specified—these are the inspection operators.

The set of the basic operators S1 is a subset of S , such that each operator from S -S 1 can be expressed in terms of the operators from S 1.

Extra inspection operators:

These are the inspection operators that are not basic inspectors.

A simple way to determine whether an operator is a constructor (basic or extra) or an inspector (basic or extra) is to check the syntax expression for the operator.

If the type being specified appears on the right hand side of the expression then it is a constructor, otherwise it is an inspection operator.

For example, in the below example, create is a constructor because point appears on the right hand side of the expression and point is the data type being specified.

But, xcoord is an inspection operator since it does not modify the point type.

A good rule of thumb while writing an algebraic specification, is to first establish which are the constructor (basic and extra) and inspection operators (basic and extra). Then write down an axiom for composition of each basic construction operator over each basic inspection operator and extra constructor operator.

Also, write down an axiom for each of the extra inspector in terms of any of the basic inspectors. Thus, if there are m1 basic constructors, m2 extra constructors, n1 basic inspectors, a nd n2 extra inspectors, we should have m1 × (m2 + n1) + n2 axioms.

However, it should be clearly noted that these m1 × (m2 + n1) + n2 axioms are the minimum required and many more axioms may be needed to make the specification complete.

Using a complete set of rewrite rules, it is possible to simplify an arbitrary sequence of operations on the interface procedures.

While developing the rewrite rules, different persons can come up with different sets of equations.

However, while developing the equations one has to be careful that the equations should be able to handle all meaningful composition of operators, and they should have the unique termination and finite termination properties.

Example :

Let us specify a data type point supporting the operations create, xcoord, ycoord, isequal; where the operations have their usual meaning.

Types: defines point uses boolean, integer

Syntax:

1. create : integer × integer → point 2. xcoord : point → integer

3. ycoord : point → integer

4. isequal : point × point → boolean

Equations:

1. xcoord(create(x, y)) = x

2. ycoord(create(x, y)) = y

3. isequal(create(x1, y1), create(x2, y2)) = ((x1 = x2)and(y1 = y2))

In this example, we have only one basic constructor (create), and three basic inspectors (xcoord, ycoord, and isequal). Therefore, we have only 3 equations.

The rewrite rules let you determine the meaning of any sequence of calls on the point type.

Consider the following expression: isequal (create (xcoord (create(2, 3)), 5),create (ycoord (create(2, 3)), 5)). By applying the rewrite rule 1, you can simplify the given expression as isequal (create (2, 5), create (ycoord (create(2, 3)), 5)). By using rewrite rule 2, you can further simplify this as isequal (create (2, 5),create (3, 5)). This is false by rewrite rule 3.

Properties of algebraic specifications

Three important properties that every algebraic specification should possess are:

Completeness:

This property ensures that using the equations, it should be possible to reduce any arbitrary sequence of operations on the interface procedures. When the equations are not complete, at some step during the reduction process, we might not be able to reduce the expression arrived at that step by using any of the equations.

There is no simple procedure to ensure that an algebraic specification is complete.

Finite termination property:

This property essentially addresses the following question:

Do applications of the rewrite rules to arbitrary expressions involving the interface procedures always terminate?

For arbitrary algebraic equations, convergence (finite termination) is undecidable

But, if the right hand side of each rewrite rule has fewer terms than the left, then the rewrite process must terminate.

Unique termination property:

This property indicates whether application of rewrite rules in different orders always result in the same answer.

Example

Let us specify a FIFO queue supporting the operations create, append, remove, first, and isempty; where the operations have their usual meaning.

Types: defines queue uses boolean, element Exception: underflow, novalue

Syntax:

1. create : ϕ → queue

2. append : queue × element → queue

3. remove : queue → queue + {underf low}

4. f irst : queue → element + {novalue}

5. isempty : queue → boolean

Equations:

1. isempty(create()) = true

2. isempty(append(q, e)) = f alse

3. f irst(create()) = novalue

4. f irst(append(q, e)) = if isempty(q) then e else f irst(q)

5. remove(create()) = underf low

6 . remove(append(q, e)) append(remove(q), e) = if isempty(q) then create( ) else

In this example, we have two basic construction operators (create and append).

We have one extra construction operator (remove). We have considered remove to be an extra construction operator because all values of the queue can be realised, even without having the remove operator.

We have two basic inspectors (first and isempty). Therefore we have 2 × 3 = 6 equations.