Imperative Programming HT23, Invariants
“When Jon Bentley assigned binary search as a problem in a course for professional programmers, he found that ninety percent failed to provide a correct solution after several hours of working on it, mainly because the incorrect implementations failed to run or returned a wrong answer in rare edge cases. A study published in 1988 shows that accurate code for it is only found in five out of twenty textbooks.” - From the Wikipedia page for binary search
Flashcards
\[\{P\} C \{Q\}\]
How can you read this Hoare triple?
When $P$ is true, executing $C$ establishes $Q$.
What is the while inference rule for a while loop containing a condition $C$, a body $\text{body}$ and an invariant $I$?
What three things must you show about a loop invariant?
- Initialisation; it is true at the first iteration
- Maintenance; if it is true at the start of a loop, it remains true for the start of the next iteration.
- Termination; when the loop terminates, the invariant gives us a useful property.
def search(a: Array[Int], x: Int) : Int = {
val N = a.size
// invariant I: a[0..i) < x <= a[j..N) && 0 <= i <= j <= N
var i = 0; var j = N
while(i < j){
val m = (i+j)/2 // i <= m < j
if(a(m) < x) i = m+1 else j = m
}
// I && i = j, so a[0..i) < x <= a[i..N)
i
}
This code seems correct, but what’s the small edge case that means it’s not mathematically correct?
def search(a: Array[Int], x: Int) : Int = {
val N = a.size
// invariant I: a[0..i) < x <= a[j..N) && 0 <= i <= j <= N
var i = 0; var j = N
while(i < j){
val m = (i+j)/2 // i <= m < j
if(a(m) < x) i = m+1 else j = m
}
// I && i = j, so a[0..i) < x <= a[i..N)
i
}
(i+j) might cause an overflow.
@Define a datatype invariant.
A property true of a datatype that is true initially, and is maintained by each operation.