[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

• Recall: Algorithms are abstract
• programs are implementations of algorithms.

• Testing can show that a program is wrong but can never show that it is (always) correct!

• Logic can prove that a program is correct.

• Usually do this in 2 parts:

1. show correct when (if) it terminates, and

2. show it terminates.

• Example follows . . .

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

 ©D.Powell&L.Allison function B(a, N, key) { ` ` NB. Needs JavaScript ON! ... }; a[1 . . ] = key: output: NEEDS JavaScript //PRE: ??? var i, lo=1, hi=N+1; while(lo < hi-1) // at least two elements {//INVARIANT: ??? var mid = Math.floor((lo+hi)/2); if( key > a[mid] ) lo=mid; else // ??? hi=mid; } // ??? if( N > 0 && a[lo] == key ) print(key + ' found at a[' + lo + ']'); else print(key + ' not found');
• show failing on bug
• correct bug, add assertions & invariant, prove correct . . .
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

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

• hi - lo `   ` is +ve and decreases

• this cannot continue forever (for an int)

• NB. reals (floats) are different!

Note dependence of proof on . . .

• Pre-condition: a[ ] is sorted and N > 0

• (Given code does not work if precondition is false.)

• Invariant, ... a[ lo .. hi - 1] ..., minus 1 is crucial for this version

• ... i.e. lo inclusive, hi exclusive ...

which corresponds to

• ... if( key >= a[mid] )

## Complexity (time and space):

• Binary search takes about log2N iterations, always

• because [__________________________]

• NB. NOT worth having a 3-way   [ >, =, < ]   test and break in the loop

• [why?]

• would lose [how much] time almost always

• but only save [how many] iterations on average

• -- Dijkstra.

## Correctness, Verification:   Summary

• Logic can prove that a program is (always) correct.

• Testing can only show that a program is

• incorrect or

• sometimes "correct".

## Prepare:

• the simple O(n2)-time sorting algorithms, e.g. insertion sort etc., and their correctness proofs.
© 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).