by Dinesh Thakur

Formal methods of specification can ensure that the specification are precise & note open to multiple interpretations. There are some desirable properties that module specifications should have. First, the specifications should be complete. That is, the given specification should specify the entire behavior of the module.


A related property is that the specifications should be unambiguous. The specifications should be easily understandable & the specification language should be such that specifications can be easily written. An important property of specifications is that they should be implementation dependent. That is, they should be given in an abstract manner.

Specifying Functional Modules


The most abstract view of a functional module is to treat it as a black box that takes in some inputs & produces some output such that the outputs have a specified relationship with the inputs. Most modules are designed to operate only on inputs that satisfy some constraints. The constraints may be on the type of input & the range of inputs. For example, a function that finds the square root of a number may be designed to operate only on the real numbers. One method for specifying modules was proposal by Hare, based on pre and post conditions. In this method constrains on the input of a module were specified by a logical assertion on the input state called pre-condition. The output was specified as a logical assertion on he output state called post-condition. As an example, consider a module sort to be written to sort a list of L integers in ascending order. The pre & post condition of this module are:

          Pre condition         :         non-null L

          Pos condition:        for all i.,

The specification states that if the input state for the module sort is non-null L, the output state should be such that the elements of L are in increasing order.

Specifying classes

Data abstraction is considered one of the most important language concepts of recent times. Various specification techniques have evolved for specifying abstract data types. One of them is the axiomatic specification technique. In this technique, the operations are not directly specified. Instead, axioms are used that specify the behavior of different interaction.


Let us use the axiomatic method by writing specifications for a stack of integers. We define a stack that has four operations


1)           Create: to create a new stack

2)           Push: to push an element on a stack.

3)           Pop: to pop the top element from the stack.

4)           Top: return the element on top of the stack.


Based on our understanding of these words, we may derive proper semantics of operations in this simple case. However. For absolutely new data types, this assumption may not hold. The specification of the stack are shown below:


1.            Stack [integer] declare

2.            create ( ) – stack;

3.            Push (stack, integer) – stack

4.            Pop (stack) – stack;

5.            Top (Stack) – integer U undefined;


A high quality SRS reduces the development cost. Hence, the quality of the SRS impacts the customer satisfaction, system validation, quality of the final software, & the software development cost.