www.Tutorialsforu.info

2.3.3 Formal and Semiformal Specifications

The proposers of formal specifications methods postulate that software development will be revolutionized by describing and modeling programs using strict syntax and semantics based on a mathematical notation. The fundamentals of formal specification are in set theory and the predicate calculus. The main advantages of formal specifications are their lack of ambiguity and their consistency and completeness, thus eliminating the many possible interpretations that often result from problem descriptions in a natural language. Of these attributes, lack of ambiguity results from the use of mathematical notation and logical symbolism. Consistency can be ensured by proving mathematically that the statements in the specification can be derived from the initial facts. However, completeness is difficult to ensure even when using formal methods of specification, since program elements can be purposefully or accidentally omitted from the specification. The original notion of applying the methods of the predicate calculus to problems in computing, and, in particular to the formal development of programs, is usually attributed to Professor Edsger W. Dijkstra (University of Texas, Austin TX, USA) who achieved considerable fame in the field of structured programming, first expressed his ideas in a book titled A Discipline of Programming. Professor David Gries (Cornell Univeristy, Ithaca NY, USA) and Edward Cohen have also made major contributions to this field.

One of the most interesting postulates made by the advocates of formal specifications is that once a program is mathematically described it can be coded automatically. In this manner it is claimed that formal specifications will eventually lead into automated programming, and thus, to the final solution of the software crisis.
In this book we have opted not to discuss the details of formal specifications for the following reasons:

1. So far, the viability of this method has been proven only for rather small programs dealing with problems of a specific and limited nature.

2. The use of this method assumes mathematical maturity and training in formal logic. It is considered difficult to learn and use.

3. Although formal specifications, program proving, and automated coding have gained considerable ground in recent years, these methods are not yet established in the systems analysis and programming mainstream. Many still consider them more an academic refinement than a practical procedure.

2.3.4 Assertions Notation

Although formal specification methods have not yet achieved the status of a practical methodology applicable in general systems analysis and programming, there is little doubt that reducing the ambiguity and inconsistency of natural languages is a desirable achievement in the software specifications stage. Some current authors of programming textbooks (including Headington and Riley) have adopted a method of program documentation which can also serve as a model for semiformal specifications. This technique, sometimes referred to as an assertion notation, consists of a specific style of comments that are inserted into the code so as to define the state of computation. Although assertions were originally proposed as a code documentation technique, the notation can also be used as a semiformal method of specification during the analysis phase. The following types of assertion are described:

ASSERT

This comment header describes the state of computation at a particular point in the code. Before this notation was suggested, some programmers inserted comments in their code with headers such as AT THIS POINT: that performed a functionally equivalent purpose. The idea of the ASSERT: header is to state what is certainly known about variables and other program objects so that this information can be used in designing and testing the code that follows.

Consider the following C++ example: a function called Power() is implemented so that it returns a float, the result of raising a float-type base to an integer power. The resulting code could be documented as follows:

Power(base, index);

// ASSERT:

// Power() == base raised to index

// (variables base and index are unchanged by call)

Certain symbols and terms are often used in the context of assertions. For example, the term Assigned is used to represent variables and constants initialized to a value. This excludes the possibility of these elements containing “garbage.” In C++ assertions the symbols && are often used to represent logical AND, while the symbol || represents logical OR regarding the terms of the assertion. The symbol == is used to document a specific value and the symbol ?? indicates that the value is unknown or undeterminable at the time. Finally, the symbol —, or the word Implies, is sometimes used to represent logical implication. The programmer should also feel free to use other symbols and terms from mathematics, logic, or from the project’s specific context, as long as they are clear, unambiguous, and consistent.
INV

This comment header represents a loop invariant. It is an assertion which is used to describe a state of computation at a certain point within a loop. The intention of the loop invariant is to document the fundamental tasks to be performed by the loop. Since the invariant is inserted inside the loop body, its assertion must be true before the body executes, during every loop iteration, and immediately after the loop body has executed for the last time. The following example in C++ is a loop to initialize to zero all the elements of an array of integers.

// ASSERT:

// All set1[0 .. sizeof (Set1)/ sizeof (int)] == ??

for (int i = 0, i <= (sizeof (Set1) / sizeof (int)), i++)

// INV:

// 0 <=i <= elements in array

Set1[]

set1(i) = 0;

// ASSERT:

// All set1[0 .. sizeof (Set1) / sizeof *int)] == 0

In this example the number of elements in an array is determined at compile time using the C++ sizeof operator. The expression:

sizeof Set1

returns the number of bytes in array Set1. This value is divided by the number of bytes in the array data type to determine the number of elements. Although this way of determining the number of elements in an array is generally valid in C++, it should be used with caution since the calculation is only permissible if the array is visible to sizeof at the particular location in the code where it is used. The loop invariant states that at this point in the loop body the index to the array (variable i) is in the range 0 to number of array elements, which can be deduced from the loop statement.