[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.

Correctness, Verification:   Introduction

Example: This is a well known algorithm with a bug. What algorithm? What bug?

©
D
.
P
o
w
e
l
l
&
L
.
A
l
l
i
s
o
n
function B(a, N, key) {
  ... };
a[1 . . ] = key:
output:
  conditional (if) ...
// 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

©
L
.
A
l
l
i
s
o
n

Note dependence of proof on . . .

Complexity (time and space):

Correctness, Verification:   Summary

Prepare:

© L.Allison, Sunday, 28-Nov-2021 04:33:48 AEDT users.monash.edu.au/~lloyd/tilde/CSC2/CSE2304/Notes/03logic.shtml
Computer Science, Software Engineering, Science (Computer Science).