Hoare Logic

Hoare logic forms the basis of all deductive verification. To illustrate Hoare logic, we first consider a smaller imperative programming language IMP.

In IMP, we have three program constructs: expressions, conditionals, and statements:

• Expression takes the form \( E := Z\ |\ V\ |\ e_1 + e_2\ |\ e_1 \times e_2 \)

• Conditional is self-explanatory: \( C := true\ |\ false\ |\ e_1 = e_2\ |\ e_1 \leq e_2 \)

• Statement consists of several different forms:

  • \(S := V := E\) (Assignment)
  • \(S_1; S_2\) (Composition)
  • if \(C\) then \(S_1\) else \(S_2\) (If)
  • while \(C\) do \(S\) (While)

Hoare Triple

In Hoare logic, we specify partial correctness of programs using Hoare triples:

\[\{P\} S \{Q\}\]

Here \(P\) is the precondition and \(Q\) is the post-condition. $S$ is a statement in IMP.

The interpretation of Hoare triple is as follows:

1. if \(S\) is executed in a state satisfying \(P\)

2. and if execution of \(S\) terminates

3. then the program state after \(S\) terminates satisfies \(Q\)

Here an example, \(\{x = 0 \} while\ true\ do\ x := 0\ \{x = 1 \}\) is a valid Hoare triple because the execution of the statement never terminates, thus satisfying the requirement posed by Hoare triple.

Thus the specification \(\{P\} S \{Q\}\) is called partial correctness spec, because it doesn’t require \(S\) to terminate.

There is also a stronger requirement called total correctness. The total correctness specification is written as:

\[ [P] S [Q]\]

Total correctness requires that if \(P\) is satisfied when executing \(S\), then \(S\) must terminate, and the post-conditional \(Q\) must be satisfied after \(S\) terminates.

Thus the example \(\{x = 0 \} while\ true\ do\ x := 0\ \{x = 1 \}\) is no longer valid because it never terminates.

In summary, we can say that Total correctness \(=\) Partial correctness \(+\) termination.

Proving Partial Correctness

We use \(\vDash \{P\} S \{Q\} \) to say a Hoare triple is valid and we use \(\vdash \{P\} S \{Q\} \) to indicate we can prove validity of a Hoare triple.

Let’s say we are given an assignment \(x := y \) with post-condition \(x > 2\). The question is, what do we need to know before the assignment happens so that the post-condition, \(x > 2\), holds afterwards?

To prove \(Q\) holds after the assignment \(x := E\), we need to show that \(Q\) with \(E\) substituting \(x\) holds before the assignment. Formally, we write it as:

\[\vdash \{Q[E / x]\}\ x := E \{Q\}\]

For example, given \( \{ x+1 = n\}\ x := x+1 \ \{x=n\} \), we know this formula is provable because we can take \(Q\), which is \(\{x=n\}\), substituting \(x\) with \(x+1\) given we need to replace it with \(E\), and we will convert \(x=n\) to \(x+1 = n\), which matches the precondition.

Here is another interesting example, given \( \{z = 2\}y:= x \{y = x\} \), this Hoare triple is valid but not provable. If we use the above substitution procedure, it will result in the precondition being \(x=x\) which is always true but is also different from the original precondition \(z=2\).

Intuitively, we can prove the post-condition \(y = x\) given the statement \(y = x\) without any assumptions, so even if we do have assumptions like \(z=2\), we should still be able to prove it, and here comes proof rule for precondition strengthening.

Proof Rule for Precondition Strengthening

Formally, we define precondition strengthening as:

\[ \frac{ \vDash \{P’\} S \{Q\}\ \ P \Rightarrow P’ }{\vdash \{P\} S \{Q\}} \]

Now, with the original formula \( \{z = 2\}y:= x \{y = x\} \), we would derive \( x= x \equiv true \). and since \(z=2 \rightarrow true\) is valid, we can now prove the formula!

A Dual: Post-Condition Weakening

Formally, we define post-condition weakening as:

\[ \frac{ \vDash \{P\} S \{Q’\}\ \ Q’ \Rightarrow Q }{\vdash \{P\} S \{Q\}} \]

What this means if that if we can prove a post-condition \(Q’\), we can always relax it to something weaker.

For example, given that \(\vdash \{true\}S\{x=y \land z=2\}\), we can prove \(\{true\}S\{x=y\}\) because \(x=y\) is a weaker condition of \( x=y \land z=2 \).

Proof Rule for Composition

For composition, we define the rule as:

\[ \frac{ \vdash \{P\}S_1\{Q\}\ \ \vdash \{Q\}S_2 \{R\} }{ \vdash \{P\}S_1;S_2\{R\} }\]

I won’t show why this is true, so this will be left as an exercise.

Proof Rule for If Statements

Naturally, we define the rule for if statement as:

\[ \frac{_{ \vdash \{P \land C\} S_1 \{Q\} }^{ \vdash \{P \land \neg C\} S_2 \{Q\} }}{ \vdash \{P\}\ if\ C\ then\ S_1\ else \ S_2 \ \{Q\} } \]

In summary, this means given we know \(P\) is true, no matter what \(C\) evaluates to, we will come to the same post-condition \(Q\). If you still don’t understand it, just stare at it for five minutes and you should figure out why this is the case:)

Proof Rule for While

To understand the proof rule for while statement, we need to first understand a simple concept: loop invariant

Loop Invariant

Loop invariant \(I\) has two properties:

1. \(I\) holds initially before the loop

2. \(I\) holds after each loop iteration

For example, given a loop

i := 0;
j := 0;
n := 0;
while i < n do
    i := i + 1;
    j := i + j

Here, \(i \leq n \) is a loop invariant but \(i < n \) isn’t.

Now, we put the properties of loop invariant \(I\) in formal terms. Given that the precondition before a loop executes is \(C\), by definition, \(I\) holds initially before the loop, we know \(I \land C\) holds.

For the second property of loop invariant, it specifies \(I\) holds after each loop iteration. So that means \(\{ I \land C\ \} S \{I\} \) holds. Formally, we express loop invariant as \( \vdash \{P \land C\} S \{P\} \).

Now, we know if a loop terminates, it must be that condition \(C\) no longer holds, meaning \( P \land \neg C \) must be true after loop terminates. This is because \(P\) is a loop invariant and always holds after each loop iteration, including termination.

Putting all this together, we form the proof rule for while loop:

\[ \frac{ \vdash \{P \land C\} S \{P\} }{ \vdash \{P\} while \ C \ do \ S\{P \land \neg C\} }\]

Inductive Loop Invariant

It’s not always the case that we can prove loop invariant is valid. Here is a counter example:

Consider precondition \( I = j \geq 1 \) and the code is:

\[i := 1; j := 1; while \ i < n\ do\ \{j := j+i; i ;= i + 1\}\]

We know that the precondition is \(I = j \geq 1\) and \(C\) (loop condition) is \(i \leq n\). So we have a Hoare triple:

\[ \{ j \geq 1 \land i \leq n \} j =j + i;\ i = i + 1; \ \{j \geq 1\} \]

We could simply set \(i = -100\), then if we execute the code once we will not be sure if the post-condition \(j \geq 1\) holds.

However, if we have strengthened invariant such as \(j \geq 1 \land i \geq 1\), the new Hoare triple will be valid. Then \(I\) will become inductive invariant because we can prove these invariant.

To put everything in action, here is an example showing how to find inductive loop invariant to prove the following Hoare triple:

\[ \{i = o \land j = o \land n = 5\} \] \[while\ i < do\ i := i + 1; \ j := j + i; \] \[\{j = 15\} \]

If we have \( j = \frac{i(i+1)}{2} \), this is a loop invariant because we can prove that:

\[\{j = \frac{i(i+1)}{2} \land i < n\} i = i + 1;\ j = j+ i\ \{j = \frac{i(i+1)}{2}\} \]

If we conjoin this condition with \(i \geq n\) as the post-condition, however, we can’t really show that \(j = 15\) is true for the given Hoare triple.

If we also add condition \(n = 5\) and \(i \leq n\), and we conjoin this with the end-loop condition \( i \geq n\), we would realize that \( i = n = 5\), and thus prove that \(j = 15\) for the given Hoare triple.

How we get \(j = \frac{i(i+1)}{2}\) is, however, not trivial to solve, and requires some human effort in program verification.

Basic Idea behind Program Verification

Automating Reasoning in Hoare Logic

It’s reasonable to automate the tedious parts of program verification: proving correctness. The basic idea to assume an oracle (human or another program) gives loop invariants but automate the rest of the reasoning.

Automating Hoare logic is based on generating verification conditions (VC). Essentially, a verification condition is formula \(\phi\) s.t. program is correct iff \(\phi\) is valid.

There are two way to generate verification conditions: forwards and backwards.

As their name suggests, a forwards analysis starts from precondition and generates formulas to prove post-condition. Forwards technique computes strongest post-conditions (sp). In contrast, backwards analysis starts from post-condition and tries to prove precondition. Backwards technique computes weakest preconditions (wp).

Here, we start from the backwards method.

Weakest Preconditions

Formally, we define the weakest precondition of \(Q\) with respect to \(S\) as \(wp(S, Q)\).

\(wp(S, Q)\) has the property that it is the weakest condition (least amount of information we need to have) that guarantees \(Q\) holds after \(S\) in any execution.

Thus, Hoare triple \( \{P\}S\{Q\} \) is valid iff \( P\Rightarrow wp(S, Q) \).

Weakest preconditions are defined inductively and follow Hoare’s proof rules:

• \(wp(x := E, Q) = Q[E/x]\)

• \( wp(s_1 ; s_2, Q) = wp(s_1, wp(s_2, Q) ) \)

• \(wp(if \ C\ then \ s_1\ else \ s_2, Q) =C \rightarrow wp(s_1, Q) \land \neg C \rightarrow wp(s_2, Q) \)

However, for loops, we might not be able to compute the weakest preconditions exactly because there might be cases where we simply don’t know the number loops executed.

Thus, we relax our requirement by computing \(awp(S,Q)\) (\(a\) stands for approximate)) instead, hoping that \(awp(S, Q)\) is weak enough to be implied by \(P\) although it may not be the weakest.

Now, assume all loops are annotated with invariants \(while \ C \ do \ [I]\ S\), we will just define \(awp(while \ C \ do \ [I]\ S, Q) \equiv I\).

However, there is another program, since \(awp\) is only an approximated condition, it doesn’t necessarily mean that if \(P \Rightarrow awp(S, Q)\), \( \{P\}S\{Q\} \) is valid. There are two reasons:

1. We don’t know if the loop invariant \(I\) provided by the oracle is correct since it might be provided by human and we know human make mistakes.

2. Even if \(I\) is correct, we don’t know if \(I \land \neg C\) is sufficient to establish \(Q\).

Thus, for each statement \(S\), we need to generate verification condition (VC) \( VC(S,Q) \) which encodes additional conditions to prove.

Verification Conditions

So how do we formulate VC generation rules for loops?

\[ VC(while\ C\ do\ [I]\ S,Q) = ?\]

First, we need to ensure that \(Q\) is satisfied after loop, which means \( I \land \neg C \Rightarrow Q \).

To show that \(I\) is actually correct, we also need \( \{I \land C\} S \{I\} \).

This implies that we need to show \( I \land C \Rightarrow awp(S, I) \). In case \(S\) contains nested loops, and also add \(VC(S, I)\)

In summary, to how that loop invariant \(I\) provided by the oracle is correct, we need to show \( I \land C \Rightarrow awp(S,I) \land VC(S, I) \).

To show \(I\) is strong enough to establish \(Q\), we need to show \( I \land \neg C \Rightarrow Q \).

Putting this together, and to answer the two reason why \(P \Rightarrow awp(S, Q)\), \( \{P\}S\{Q\} \) might not be valid, VC for a while loop \( S’ = while \ C \ do \ \{I\} \) is expressed as:

\[ VC(S’, Q) = (I \land C \Rightarrow awp(S, I) \land VC(S, I) ) \land (I \land \neg C \Rightarrow Q) \]

In essence, verification condition simply stands for additional checks we need to verify before we can claim that, if an approximated precondition \(P\) is valid, \( \{P\} S \{Q\} \).

The verification condition for other statements is as follows:

1. For assignment, we don’t need any additional checks for precondition because if \( P \Rightarrow wp(S, Q) \), it implies that \( \{P\} S \{Q\} \) is valid. Thus, \( VC(x:= E, Q) = true \).

2. For composition, we have \( VC(s_1 ; s_2, Q) = VC(s_2, Q) \land VC(s_1, awp(s_2 , Q)) \).

3. For if statement, we have \( VC(if \ C \ then \ s_1\ else \ s_2, Q) = VC(s_1, Q) \land VC(s_2, Q) \).

Quick question: for if statement, why don’t we instead use verification condition generation rule: \( C \Rightarrow VC(s_1, Q) \land \neg C \Rightarrow VC(s_2, Q) \)?

Here is a counter example. Suppose we have \( S = if\ (x > 0) \ while (*) x - -; else \ skip\), and we have given loop invariant \(x \geq 0\).

If we use the original rule \( VC(s_1, Q) \land VC(s_2, Q) \), according to the verification condition generation rule for while loop, we would have to verify the loop invariant \(I\) is correct, and thus \(VC(S, I) \equiv \{ x \geq 0 \} x - - \{ x \geq 0 \} \), obviously, this not true, and we can use this VC.

However, if we instead use the rule \( C \Rightarrow VC(s_1, Q) \land \neg C \Rightarrow VC(s_2, Q) \). The VC would become \( x > 0 \Rightarrow (\{ x \geq 0 \} x - - \{ x \geq 0 \}) \), which is valid, and we will include the wrong VC. Thus we can’t use this VC generation rule.

Verification of Hoare Triple

Thus, to show validity of Hoare triple \( \{P\} S \{ Q \} \), we need to compute:

1. \( awp(S, Q) \)

2. \( VC(S, Q) \)

Therefore, a Hoare triple is valid if the following formula holds:

\begin{equation}\tag{*} VC(S, Q) \land P \rightarrow awp(S, Q) \end{equation}

Thus, if we can prove the validity of the above equation *, we know the program obeys specification.