[Subject home],
[FAQ],
[progress],
Bib',
Alg's,
C ,
Java- L.A.,
Sunday, 28-Nov-2021 04:33:48 AEDT Instructions:
Topics discussed in these lecture notes are examinable
unless otherwise indicated.
You need to follow instructions,
take more notes &
draw diagrams especially as [indicated] or
as done in lectures,
work through examples, and
do extra reading.
Hyper-links not in [square brackets] are mainly for revision,
for further reading, and for lecturers of the subject.

// ASSERT P
if( Q )
// ASSERT P and Q
...
else
// ASSERT P and not Q
...

true case...

// key in a[] iff key in a[lo..hi-1]
if( key >= a[mid] )
// key in a[] iff key in a[lo..hi-1]
// and key >= a[mid]
lo = mid;
// key in a[] iff key in a[lo..hi-1]
else
...

false case...

// key in a[] iff key in a[lo..hi-1]
if( key >= a[mid] )
...
else
// key in a[] iff key in a[lo..hi-1]
// and key < a[mid]
hi = mid;
// key in a[] iff key in a[lo..hi-1]

put the two branches together:-

// key in a[] iff key in a[lo..hi-1]
if( key >= a[mid] )
lo = mid;
else
hi = mid;
// key in a[] iff key in a[lo..hi-1]

loop...

// I
while( C )
{ // INVARIANT: I
body;
// I
}
// I and not C

An invariant is [____________________________].

while( lo < hi - 1 )
{ // key in a[] iff key in a[lo..hi-1]
loop body for
binary search
}
// key in a[] iff key in a[lo..hi-1]
// and lo >= hi-1
// in fact lo = hi-1
// so key in a[] iff key == a[lo]

Termination

( lo < hi-1 ) => ( hi >= lo+2 ) => ( lo < mid < hi )