Discrete Mathematics

304 DISCRETE MATHEMATIC..._

________________________

_

(d) p

&&

! B implies Q;

then the loop is correct, in that it has the desired effect summarized

by

postcondition Q.

Finding the invariant is the difficult part.

Often you must start from the desired result and work back-

wards.

10.3

LINEAR

SEARCH

In this section we will discuss the correctness

of

linear search. The problem is as follows. Given an array A

of

elements:

class Element {

public:

Element ( const Element & );

Element

& operator = ( const Element &

);

boot

operator = = ( const Element & );

int operator < ( const Element & );

}

and a specific element x,find the index ...