Algebraic Specification

Specific Instructional Objectives

At the end of this lesson the student will be able to:

· Explain algebraic specification and its use.
· Explain how algebraic specifications are represented.
· Develop algebraic specification of simple problems.
· Identify the basic properties that a good algebraic specification should satisfy.
· State the properties of a structured specification.
· State the advantages and disadvantages of algebraic specifications.
· State the features of an executable specification language (4GL)with suitable examples.

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 specification of abstract data types. Various notations of algebraic specifications have evolved, including those based on OBJ and Larch languages.

Representation of algebraic specification

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; {I, +, -, *, /}. In contrast, alphabetic strings together with operations of concatenation and length {A, 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 the algebra, in turn, is called a sort of the algebra. To define a heterogeneous algebra, we first need to specify its signature, the involved operations, and their domains and ranges. Using algebraic specification, we define the meaning of a set of interface procedure 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 is specified.

Exceptions 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. For example, in a queue, possible exceptions are novalue (empty queue), underflow (removal from an empty queue), etc.

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, the append operation takes a queue and an element and returns a new queue. This is represented as:

append : queue x element ® queue

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. For example, a rewrite rule to identify an empty queue may be written as:

isempty(create()) = true

By convention each equation is implicitly universally quantified over all possible values of the variables. Names not mentioned in the syntax section such as ‘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:

1. 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 element of the type being specified. For example, ‘create’ and ‘append’ are basic construction operators for a FIFO queue.

2. Extra construction operators. These are the construction operators other than the basic construction operators. For example, the operator ‘remove’ is an extra construction operator for a FIFO queue because even without using ‘remove’, it is possible to generate all values of the type being specified.

exception conditions are used in the later sections of an algebraic specification. For example, in a queue, possible exceptions are novalue (empty queue), underflow (removal from an empty queue), etc.

Syntax section:-

append : queue x element ® queue

Equations section:-

isempty(create()) = true

uses boolean, integer.

Exceptions:

underflow, novalue

Syntax:

1. create : f ® queue

2. append : queue x element ® queue

3. remove : queue ® queue + {underflow}

4. first : queue ® element + {novalue}

5. isempty : queue ® boolean

Equations:

1. isempty(create()) = true

2. isempty((append(q,e)) = false

3. first(create()) = novalue

4. first(append(q,e)) = is isempty(q) then e else first(q)

5. remove(create()) = underflow

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

append(remove(q),e)

In this example, there are two basic constructors (create and append), one extra construction operator (remove) and two basic inspectors (first and empty). Therefore, there are 2 x (1+2) + 0 = 6 equations.

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. 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. Essentially, to determine this property, the answer to the following question needs to be checked: Can all possible sequence of choices in application of the rewrite rules to an arbitrary expression involving the interface procedures always give the same number? Checking the unique termination property is a very difficult problem.

Structured specification

Developing algebraic specifications is time consuming. Therefore efforts have been made to device ways to ease the task of developing algebraic specifications. The following are some of the techniques that have successfully been used to reduce the effort in writing the specifications.

§ Incremental specification. The idea behind incremental specification is to first develop the specifications of the simple types and then specify more complex types by using the specifications of the simple types.

§ Specification instantiation. This involves taking an existing specification which has been developed using a generic parameter and instantiating it with some other sort.

Advantages and disadvantages of algebraic specifications

Algebraic specifications have a strong mathematical basis and can be viewed as heterogeneous algebra. Therefore, they are unambiguous and precise. Using an algebraic specification, the effect of any arbitrary sequence of operations involving the interface procedures can automatically be studied. A major shortcoming of algebraic specifications is that they cannot deal with side effects. Therefore, algebraic specifications are difficult to interchange with typical programming languages. Also, algebraic specifications are hard to understand.

Executable specification language (4GLs).

If the specification of a system is expressed formally or by using a programming language, then it becomes possible to directly execute the specification. However, executable specifications are usually slow and inefficient, 4GLs³ (4^th Generation Languages) are examples of executable specification languages. 4GLs are successful because there is a lot of commonality across data processing applications. 4GLs rely on software reuse, where the common abstractions have been identified and parameterized. Careful experiments have shown that rewriting 4GL programs in higher level languages results in up to 50% lower memory usage and also the program execution time can reduce ten folds. Example of a 4GL is Structured Query Language (SQL).

For the following, mark all options which are true.

1. An SRS document normally contains

□ Functional requirements of the system √

□ Module structure

□ Configuration management plan

□ Non-functional requirements of the system √

□ Constraints on the system √

2. The structured specification technique that is used to reduce the effort in writing specification is

□ Incremental specification

□ Specification instantiation

□ Both of the above √

□ None of the above

3. Examples of executable specifications are

□ Third generation languages

□ Fourth generation languages √

□ Second-generation languages

□ First generation languages

Mark the following as either True or False. Justify your answer.

1. Functional requirements address maintainability, portability, and usability issues.

Ans.: - False.

Explanation: - The functional requirements of the system should clearly describe each of the functions that the system needs to perform along with the corresponding input and output dataset. Non-functional requirements deal with the characteristics of the system that cannot be expressed functionally e.g. maintainability, portability, usability etc.

1. The edges of decision tree represent corresponding actions to be performed according to conditions.

Ans.: - False.

Explanation: - The edges of decision tree represent conditions and the leaf nodes represent the corresponding actions to be performed.

2. The upper rows of the decision table specify the corresponding actions to be taken when an evaluation test is satisfied.

Ans.: - False.

Explanation: - The upper rows of the table specify the variables or conditions to be evaluated and the lower rows specify the corresponding actions to be taken when an evaluation test is satisfied.

3. A column in a decision table is called an attribute.

Ans.: - False.

Explanation: - A column in a decision table is called a rule. A rule implies that if a condition is true, then execute the corresponding action.

4. Pre – conditions of axiomatic specifications state the requirements on the parameters of the function before the function can start executing.

Ans.: - True.

Explanation: - 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.

5. Post – conditions of axiomatic specifications state the requirements on the parameters of the function when the function is completed.

Ans.: - True.

Explanation: - The post-conditions are the conditions that must be satisfied when a function completes execution for the function to be considered to have executed successfully. Thus, the post-conditions are essentially constraints on the results produced for the function execution to be considered successful.

1. Homogeneous algebra is a collection of different sets on which several operations are defined.

Ans.: - False.

Explanation: - A heterogeneous algebra is a collection of different sets on which several operations are defined. But homogeneous algebra consists of a single set and several operations; {I, +, -, *, /}.

2. Applications developed using 4 GLs would normally be more efficient and run faster compared to applications developed using 3 GL.

Ans.: - False.

Explanation: - Even though 4th Generation Languages (4 GLs) reduce the effort for development; it is normally inefficient as these are more general-purpose languages. If somebody rewrite 4 GL programs in higher level languages (i.e. 3GLs), it might result in upto 50% lower memory requirements and also the program can run upto 10 times faster.