# Notes - Imperative Programming HT23, Invariants

> Source: https://ollybritton.com/notes/uni/prelims/ht23/ip/notes/invariants/ · Updated: 2023-01-23 · Tags: uni, notes

- [Course - Imperative Programming I and II HT23](https://ollybritton.com/notes/uni/prelims/ht23/ip/)

> "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](https://en.wikipedia.org/wiki/Binary_search#Implementation_issues)

### 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$?::
$$
\frac{ \{ C \text{ and } I \} \text{body} \{I\} \space}{\{I\}\text{while(C)body} \{\text{I and not C}\}\space}
$$

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.

```scala
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?::
`(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.

### Programs
Program a mathematically correct version of binary search that finds $i$ such that
$$
a[0\ldots i) < x \le a[i\ldots N)
$$
using invariants.::
Todo.

@todo~

---
Olly Britton — https://ollybritton.com. Machine-readable index: https://ollybritton.com/llms.txt