Page 195 - DCAP507_SYSTEM_SOFTWARE

Unit 12: Formal Systems and Programming Languages

12.2.6 The Development of an Axiomatic Spec of a Function Notes

 Institute the range of the input parameters over which the function is proposed to behave
properly. Identify the input parameter constraints as a predicate.

 State a predicate defining a condition which must hold on the output of the function if it
behaves properly.
 Establish what changes (if any) are made to the function's input parameters and state
these.
 Merge these into pre- and post-conditions for the function.

Example: An Example: Search
function Search (X:INTEGER_ARRAY;
Key:INTEGER) return INTEGER;

Pre: $ i Î X'FIRST..X'LAST:X(i) = Key
Post: X''(Search(X,Key)) = Key and X = X''

 The input array is unaffected by the search.
 Returns the value of the index of the element which is equivalent to the key.9

Example: Search of an Ordered Array

The specification now involves an additional clause in the pre-condition.
function Search (X:INTEGER_ARRAY;
Key:INTEGER) return INTEGER;

Pre: $ i Î X'FIRST..X'LAST: X(i) = Key Ù
" i,j Î X'FIRST..X'LAST: i < j Ù X(i) < = X(j)
Post: X''(Search(X,Key)) = Key and X = X''

12.2.7 The Use of an Error Predicate

 Specifications should also set out the behaviour of a constituent if it is presented with
unforeseen input.
 One strategy is to have a number of pre/post-condition pairs depending on the number of
erroneous input ranges.
The Use of an Error Predicate function Search (X:INTEGER_ARRAY; Key:INTEGER) return
INTEGER;

Pre: $ i Î X'FIRST..X'LAST: X(i) = Key
Post: X''(Search(X,Key)) = Key Ù X = X''
Error: Search(X,Key) = X'LAST + 1

LOVELY PROFESSIONAL UNIVERSITY 189