Hoare logic is a way to check the correctness of computer programs. It is basically a set of rules which one can follow to efficiently and systematically decide the correctness of a program.

When I speak of correctness, I am checking if the program “works” like its supposed to — according to some given specifications.

This correctness can be broadly classified into partial and total correctness.

Partial correctness is “weaker” than total correctness as the names clearly imply.

A program can be described as \(\{Pre \space condition\} \space Program \space \{Post \space condition\}\)

What this means is that for the program to be executed, the pre-condition must be satisfied. And, once that has happened, and if the program terminates, the result would satisfy the post-condition.

A program is deemed to be partially correct if one can say that if the precondition is true, then the expected result would satisfy the post condition assuming that the program terminates.

This assumption of termination weakens partial correctness. Any program which fails to terminate also satisfies this because one can say that it would have given the right result if it had terminated.

On the other hand, we have total correctness, which can be attributed to a program only if it satisfies partial correctness as well as terminates, allowing us to avoid making any assumptions regarding the termination of said program.

An important question arises here: if total correctness implies partial correctness and partial correctness is so weak compared to total correctness, why do we even check for partial correctness?

The answer lies in the fact that total correctness is sometimes very hard to prove. Sometimes, its easier and more efficient to prove partial correctness. Moreover, once partial correctness is proven, a termination condition can be found, making it possible to prove total correctness. This is why partial correctness is used.

Of course, Hoare logic works with both types of correctness, but this post will deal only with partial correctness. Hoare logic is used with imperative programming languages, which work with different states of variables, like C, and assembly languages. Click here for more information regarding imperative languages.

Hoare logic involves a few simple constructs. This post will focus on assignment, conditionals and sequencing — all with respect to partial correctness.

Assignment

Consider the example of a typical hoare logic implementation, with the pre and post condtions written in predicate or propositional logic, and the program written in C.

\(/* Precondition: x = 3 \wedge y = 4 */\)
\(\qquad x = x + 1;\)
\(\qquad y = y - 1;\)
\(/*Postcondtion: x = 4 \wedge y = 3*/\)

The program is simple enough: x is incremented by 1 and y is decremented by 1. The precondition states that when x = 3 and y = 4, the program will be executed and the result should satisfy the post condition. The single “=” in the pre and post conditions, which are written between /* */, works as an equality operator and not the overloaded assignment operator we associate with C and other programming languages.

The assignment construct is simple and can be expressed as the following proof rule.

\[\frac{}{/*\psi[E/x]*/ \space x = E \space /*\psi*/}Assignment\]

It means that the rule has no premises and is akin to an axiom. The precondition must be satisfied after replacing every free occurence of $x$ with $E$ in $\psi$. Then, the program assigns $E$ to $x$, following which, the post condition, $\psi$ holds true.

Sequencing

This rule allows us to combine the pre and post conditions of several pieces of the program into a single pre-condition, a program with several statements and a single post condition.

The proof rule is simple:

\[\frac{/*\phi*/ \space K_1 \space /*\psi*/ \qquad /*\psi*/ \space K_2 \space /*\Gamma */}{/*\phi*/ \space K_1; \space K2 \space /*\Gamma*/}Composition\]

A simple example:
\(/* Pre: x = 3 */\)
\(\qquad x = x + 1;\)
\(/*x = 4 */\)
\(\qquad x = x - 3;\)
\(/*Post: x = 1*/\)

This can be simplified by eliminating $/x=4/$ the post condition of the first part of the program and the pre condition of the last part of the program:

\(/* Pre: x = 3 */\)
\(\qquad x = x + 1;\)
\(\qquad x = x - 3;\)
\(/*Post: x = 1*/\)

Conditional Statements

The conditional statement construct is one of the hardest in my opinion, but with a little practise, it starts to make sense.

The proof rule may seem a bit complicated: \(\frac{/*\phi \wedge A*/ \space K_1 \space /*\psi*/ \qquad /*\phi \wedge \neg A*/ \space K_2 \space /*\psi */}{/*\phi*/ \space if A \space \{K_1\} \space else \space \{K2\} \space /*\psi*/}Composition\)

Given an if-else block, the pre-condition of the block must be a common pre condition of both the if and else parts. The above proof rule has $A$ as the if condition and $\phi$ as the “common” part which ends up becoming the precondition. Its easier to explain with an example.

Consider this:
\(/* Pre: T */\)
\(if (\space y \ge 0)\)
\(\qquad x = y;\)
\(else\)
\(\qquad x = -y;\)
\(/*Post: x = |y|*/\)

Let us try and write the precondition for the else block. Of course, for control to enter the else part, y must be less than 0. Also, because the construct within the else block is an assignment, we can use the assignment proof rule discussed above. Thus, else block precondition can be written as:

\(else\)
\(/* y \lt 0 \wedge \space |y| = -y */\)
\(\qquad x = -y;\)

Similarly, the if part can be written as:

\(if (\space y \ge 0)\)
\(/* y \ge 0 \wedge \space |y| = y */\)
\(\qquad x = y;\)

But the first part of both pre-conditions is redundant — that part is obvious from the design of the if-else block. Next, to obtain the precondition of the entire if-else block, we must look for something common between the indivisual pre-conditions of the if and else parts, something which would be required to be true irrespective of whether control enters the if or the else block. In this example, it is pretty easy to see that there is no such “common” ground. Thus, we can always prepend a $TRUE$ to both conditions and consider this our common term.

Ultimately, our pre-condition becomes $T$ or trivially true.

On that note, I end this post. The partial correctness while loop construct and validity checking will be discussed in the next post.