5.1 Hoare Logic

“I conclude that there are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies and the other way is to make it so complicated that there are no obvious deficiencies.

The first method is far more difficult.” - C. A. R. Hoare

Logic is the art and science of correct reasoning, and one of the main ways that programmers reason in determining whether code is correct or not.

Hoare Logic is one formal approach to reasoning about imperative code, due to C. A. R. (“Tony”) Hoare, who also invented the Quicksort algorithm and the null pointer.

Although Hoare Logic is an underlying technology used by many systems that try to automate the verification of code, modern programmers rarely apply it by hand. However, the high-level concepts and vocabulary remain important, because they shed light on what aspects of code are most useful to think about, and to document.

A precondition is a logical formula that is (or will be) true when we start executing a piece of code. > A postcondition is a logical formula that will be true after the code finishes, assuming the precondition was true when the code started. > The classical “Hoare Triple” Notation >\[ >\{\ P\ \}\ \ \mathtt{\ldots code\ldots}\ \ \{\ Q\ \} >\] >says that \(P\) is the precondition of the code and that \(Q\) is the postcondition, i.e., that “if \(P\) is true, and then the code executes, then afterwards \(Q\) will be true.”

Here are some valid Hoare triples: > >\[ >\begin{array}{lll} > \{\ x=3 \ \} & \mathtt{x=x+1} &\{\ x=4\ \}\\[10pt] > \{\ \mathrm{even}(x) \ \} & \mathtt{x=x+1} &\{\ \mathrm{odd}(x)\ \}\\[10pt] > \{\ \mathrm{prime}(x+1) \ \} & \mathtt{x=x+1} &\{\ \mathrm{prime}(x)\ \}\\ >\end{array} >\]

Preconditions

A precondition is a formula that is true when we start executing a piece of code.

Depending on context, a precondition could arise in several ways. It could be a pure hypothetical ( I wonder what the code would do if we ran it under these conditions? ) Or, it could reflect the specific context of the code in a larger system: ( When our program reaches this part of the code, we can guarantee that … is true. ).

But one of the most common uses of preconditions in practice is to use them as documented requirements for the code ( Don’t run this code unless …).

For example, documentation for the C++ Standard Library is full of these sorts of preconditions. It tells you exactly what invoking pop_back() on a vector<T> will do as long as the vector object is non-empty when the member function is invoked. ## Postconditions

A postcondition is a formula that will be true after code finishes, as long as the corresponding precondition was true when the code started.

Postconditions often appear in code simply as documentation for “what the code does”.

The traditional Hoare Logic approach mentioned above is based on Partial Correctness, meaning that the postcondition has to be true if the code terminates, but doesn’t gurantee anything if the code runs forever. In programming practice, we often prefer Total Correctness, which further requires that the code will terminate. ## Loop Invariants

An invariant is a formula that is “preserved by” code, i.e., if it’s true when we start the code, then it’s still true when the code finishes.

A Representation Invariant is a statement about a data structure that is true before and after every operation on that data structure.

For example, the fact that a Binary Search Tree has keys in left-to-right order is a representation invariant. Insertion into a BST if the tree is only guaranteed to work if the keys in the tree are properly ordered, but then the resulting larger tree is guaranteed to still be properly ordered.

A Loop Invariant is a formula that is true before and after every iteration of a loop.

Loop invariants are the main way that Hoare Logic reasons about code with loops. If a loop invariant \(I\) is true when a while loop begins, and each iteration of the loop preserves the truth of \(I\), then even if we don’t know how many iterations will happen at run-time, we can be sure that \(I\) remains true when the while loop finishes.

Although this may seem artificial, a good loop invariant can summarize the key reason how and why looping code works. For loops that are at all complex or clever, documenting the loop invariant can be a huge help to the readers (and often even the writer) of the code.

Question: Why does the following code work?
>(i.e., if the code starts with n == n0, why will x == n0 at the end?) > >> { n == n0 >= 0} > > x = 0 > > while ( n != 0 ): > x = x + 1 > n = n - 1 > > { x == n0 } > > >The key insight is the loop invariant x + n = n0. > >- This is true when the loop starts (because n == n0 and x == 0). >- If x + n = n0 is true at the start of an interation of the loop, it’s still true at the end; if x increases and n decreases, their sum hasn’t changed. >- x + n = n0 guarantees the desired postcondition, because it’s true when the loop terminates (and n != 0 is false), in which case n == 0 and so x == n0.

Question: Why does the following code work? > >Note:
> fib(0) = 0, fib(1) = 1, fib(2) = 1, fib(3) = 2, fib(4) = 3, fib(5) = 8, and so on. > >> { x == 0 and y == 1 and i == 1 and n>=1 } > > while ( i != n ): > y = x + y > x = y - x > i = i + 1 > > { y == fib(n) } > > >The key insight is the loop invariant x=fib(i-1) and y=fib(i). > >- This is true when the loop starts (because i == 1 and x == fib(0) and y == fib(1)). >- If x and y are two consecutive Fibonacci numbers, then the first two lines of the loop switch them to the next larger pair of Fibonacci numbers and i increases by one, so the loop invariant remains true. >- x=fib(i-1) and y=fib(i) guarantees the desired postcondition, because it’s true when the loop terminates (and i != n is false), in which case i == n and so y == fib(n).

Question: Why does the following code work? > >> { m = m0 > 0 ∧ n = n0 > 0 } > > while ( m != n ): > if ( m < n ): > n = n-m > else: > m = m-n > > { m = gcd(m0,n0) } > > >The key insight is the loop invariant gcd(m,n) = gcd(m0,n0). > >- This is trivially true when the loop starts. >- The subtraction in the loop doesn’t change the gcd of n and m (because number theory tells us \(\mathrm{gcd}(a,b)=\mathrm{gcd}(a-b,b)\), i.e., any divisor of \(a\) and \(b\) also divides their difference), so if gcd(m,n) = gcd(m0,n0) before an iteration of the loop, it’s still true afterwards. >- gcd(m,n) = gcd(m0,n0) guarantees the desired postcondition, because it’s true when the loop terminates (and m != n is false), in which case m == n and so m == gcd(m,n) == gcd(m0,n0).

Insertion Sort has a loop where i iterates through the indices of an array a, and maintains the invariant that elements a[0..i-1] are sorted and the elements a[i..] are unchanged from the start of the algorithm. Each iteration takes the first unsorted element a[i] and inserts it into the correct position, resulting in a larger prefix of the input that has been sorted. > >Selection Sort also has a loop where i iterates through the indices of an array a, but works differently. It maintains the invariant that elements a[0..i-1] have their final values (i.e., the i smallest input values, in order) and that elements a[i..] contains the remaining (larger) input values in some unknown order. Each iteration finds the smallest of the remaining elements and swaps it into the correct position, resulting in a larger prefix of the array that have their final, sorted values.

For loops whose purpose or operation is not clear at a glance, documenting the loop invariant (e.g., as a comment) is often amazingly helpful for future readers (including your future self).

Being precise about the invariant can even help avoid off-by-one errors and get the code right in the first place!

Previous: 4.9 Negation in Prolog

Next: 5.2 Countability