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?

• show failing on bug
• correct bug, add assertions & invariant, prove correct . . .

// ASSERT  P

if( Q )

  // ASSERT  P and Q

  ...

else

  // ASSERT  P and not Q

  ...

// 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

  ...

// 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]

// I

while( C )

  { // INVARIANT: I

    body;

    // I
  }

// I and not C

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 log₂N 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(n²)-time sorting algorithms, e.g. insertion sort etc., and their correctness proofs.