Definition. Hoare triple - total correctness [003z]

December 5, 2025

The classical hoare triple \(\{P\}\ s\ \{Q\}\) only captures the notion of partial correctness, meaning that if the program terminates, then the postcondition \(Q\) holds given that the precondition \(P\) held before execution. However, it does not guarantee that the program will terminate. To capture both correctness and termination, we define the total correctness Hoare triple denoted as:

\[ [P]\ s\ [Q] \]

The total correctness Hoare triple asserts that:

\[ \sigma \vDash P \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \land \sigma ' \vDash Q \]

Or equivalently viewing the conditions as assertions on memory states:

\[ P(\sigma ) \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \land Q(\sigma ') \]

The central difference we can observe here is with the usage of a conjunction with the postcondition as opposed to an implication. This means that for total correctness, if the precondition \(P\) holds in the initial state \(\sigma \), then there must exist a final state \(\sigma '\) such that executing the statement \(s\) from \(\sigma \) leads to \(\sigma '\) and the postcondition \(Q\) holds in that final state. Whereas in the case of partial correctness, if we had non-termination, the postcondition could be vacuously true.

For the sake of completeness let's also show how we might implement this in lean:


  def TotalHoareTriple {P Q : Condition} (c : Stmt) : Prop :=
    ∀ σ, P σ → ∃ σ', (c, σ) ⇓ₛ σ' ∧ Q σ'

Context

VU-VFS-2025. Lecture 5 - Nano and Hoare Logic [003n]

December 2, 2025

Semantics and Evaluation

December 2, 2025

Definition. Simple Imperative Language - Syntax [003t]

December 4, 2025

We define the syntax of a simple imperative programming language, using the followng bnf grammar:

Definition. Simple Imperative Language - Semantics [003u]

December 4, 2025

We can divide the environmental big-step semantics of our simple language into three parts:

Expression evaluation: Describes how arithmetic expressions are evaluated to numbers.
Boolean expression evaluation: Describes how boolean expressions are evaluated to boolean values (true/false).
Statement execution: Describes how statements are executed, transforming an initial state (environment) into a final state.

The general big-step environmental evalutation rule is denoted as:

\[ \langle t, \sigma \rangle \Downarrow v \]

Here:

We have some starting term \(\texttt {t}\) (which can be an expression, boolean expression, or statement), along with some state \(\sigma \).
The evaluation results in some value \(\texttt {v}\) (which can be a number, boolean value, or new state).

A quick aside here to deconstruct the term big-step environmental evaluation:

We say that this evaluation is big-step as it assumes some arbitrary state of intermediate steps, meaning that within big step semantics we do not care about intermediate computation only about some input expression and the final output value. A simple analogue to make here is that big-step semantics are akin to a teacher asking you to only show ur final answer to a math problem rather than all the steps you took to get there.
We say that this evaluation is environmental (as opposed to being substitution based) as we explicitly keep track of a state \(\sigma \) which maps variables to their values. This is in contrast to substitution based semantics where variable occurrences are replaced directly with their values in expressions.

The state \(\sigma : \texttt {String} \to \mathbb {Z}\) represents a mapping from variables (commonly strings) to their corresponding values (numbers). We denote the updated state after assigning a value to a variable \(\texttt {x}\) as:

\[ \sigma [x \mapsto n] \]

This means that in the new state, the variable \(\texttt {x}\) now maps to the number \(\texttt {n}\), while all other variable mappings remain unchanged from the original state \(\sigma \).

Expression evaluation

December 4, 2025

Boolean expression evaluation

December 4, 2025

Statement evaluation

December 4, 2025

Quiz. Simple Imperative Language - Evaluation [003v]

December 4, 2025

What does the following evaluate to? \[ \langle (x := x - 1), \sigma [x \mapsto 2] \rangle \]
What does the following evaluate to? \[ \langle \texttt {if } x + 1 \leq 3 \texttt { then } x := x - 1, \sigma [x \mapsto 1] \rangle \]
What does the following evaluate to? \[ \langle \texttt {while } (x + 1 \leq 3) \texttt { then } x := x - 1, \sigma [x \mapsto 1] \rangle \]
Is the following a total function? \[ \langle e, \sigma \rangle \Downarrow n \]
Is the following a total function? \[ \langle s, \sigma \rangle \Downarrow \sigma ' \]

Solution.

December 4, 2025

Starting in the state \(x \mapsto 2\) we evaluate \(x := x - 1\) to the state \(x \mapsto 1\)
Starting in the state \(x \mapsto 1\), we first evaluate the condition \(x + 1 \leq 3\): \[ \begin {align*} \langle x + 1, \sigma [x \mapsto 1] \rangle &\Downarrow 2 \\ \langle 3, \sigma [x \mapsto 1] \rangle &\Downarrow 3 \\ \langle 2 \leq 3, \sigma [x \mapsto 1] \rangle &\Downarrow \texttt {true} \end {align*} \] Since the condition evaluates to true, we then evaluate the then-branch \(x := x - 1\): \[ \begin {align*} \langle x - 1, \sigma [x \mapsto 1] \rangle &\Downarrow 0 \\ \langle x := 0, \sigma [x \mapsto 1] \rangle &\Downarrow \sigma [x \mapsto 0] \end {align*} \]
We again start by evaluating the condition \[ \begin {align*} \langle x + 1, \sigma [x \mapsto 1] \rangle &\Downarrow 2 \\ \langle 3, \sigma [x \mapsto 1] \rangle &\Downarrow 3 \\ \langle 2 \leq 3, \sigma [x \mapsto 1] \rangle &\Downarrow \texttt {true} \end {align*} \] Since we can see that the body of the loop only decreases \(x\), we are stuck in an infinite loop: \[ \begin {align*} \langle x := x - 1, \sigma [x \mapsto 1] \rangle &\Downarrow \sigma [x \mapsto 0] \\ \langle \texttt {while } (x + 1 \leq 3) \texttt { do } x := x - 1, \sigma [x \mapsto 0] \rangle &\Downarrow \sigma [x \mapsto -1] \\ \langle \texttt {while } (x + 1 \leq 3) \texttt { do } x := x - 1, \sigma [x \mapsto -1] \rangle &\Downarrow \sigma [x \mapsto -2] \\ &\vdots \end {align*} \]
Yes, for every expression \(e\) and state \(\sigma \), there exists a number \(n\) such that \[ \langle e, \sigma \rangle \Downarrow n \] This follows from the fact that expressions are finite syntax trees built from a finite set of rules, and each rule can be evaluated in a finite number of steps.
No, there exist statements \(s\) and states \(\sigma \) for which there is no resulting state \(\sigma '\) such that \[ \langle s, \sigma \rangle \Downarrow \sigma ' \] For example, consider the while-loop \[ \texttt {while } (x + 1 \leq 3) \texttt { do } x := x - 1 \] starting from the state \(\sigma [x \mapsto 1]\). As shown in the previous question, this loop does not terminate, and thus there is no resulting state \(\sigma '\).

Hoare Logic

December 2, 2025

Definition. Hoare triple - partial correctness [003x]

December 5, 2025

The basic unit of reasoning or judgement of the partial correctness of a program is the Hoare triple denoted as:

\[ \{P\}\ s\ \{Q\} \]

where:

\(P\) represents the precondition which must hold true before the execution of the statement \(s\).
\(Q\) represents the postcondition which must hold true after the execution of the statement \(s\), provided that \(P\) was true before execution.

If we consider a variable state \(\sigma : \texttt {String} \to \mathbb {Z}\) mapping variable names to integer values, then we can define the partial correctness condition of a Hoare triple as follows:

\[ \sigma \vDash P \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \to \sigma ' \vDash Q \]

What this says is that: if the precondition \(P\) holds in the initial state \(\sigma \), and if executing the statement \(s\) from that state leads to a new state \(\sigma '\), then the postcondition \(Q\) must hold in the new state \(\sigma '\).

In a more programmatic sense we can understand the pre and postconditions as assertions on the memory state \(\sigma \), in other words they represent a function \(A : (\texttt {String} \to \mathbb {Z}) \to \texttt {Prop}\) that evaluates to true or false based on the values of the variables in the state. Thus, we can rewrite the Hoare triple condition as:

\[ P(\sigma ) \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \to Q(\sigma ') \]

Or in lean equivalently as:


  abbrev Condition := Memory -> Prop

  def HoareTriple {P Q : Condition} (c : Stmt) : Prop :=
    ∀ σ σ', P σ → (c, σ) ⇓ₛ σ' → Q σ'

A note here is that we are using some custom notation for the big-step semantics relation. The notation \(\Downarrow _s\) here simply means the big step evaluation relation for statements.

In general for a Hoare triple we denote its validity as:

\[ \vDash \{P\}\ s\ \{Q\} \]

Quiz. Hoare triple evaluation [003y]

December 5, 2025

Asses the validity of each of the following Hoare triples.

\(\{x = 0 \}\ x := x + 1\ \{x = 1\}\)
\(\{x = 0 \land y = 1\}\ x := x + 1\ \{x = 1 \land y = 2\}\)
\(\{x = 0 \land y = 1\}\ x := x + 1 \{x = 1 \lor y = 2\}\)
\(\{x = 0\}\ \texttt {while}\ \top \ \texttt {do}\ x := x + 1\ \{x = 1\}\)

Solution.

December 5, 2025

Valid. If \(x = 0\) before execution, then after executing \(x := x + 1\), \(x\) will be \(1\).
Invalid. While \(x\) will be \(1\) after execution, \(y\) remains \(1\), so the post-condition \(y = 2\) does not hold.
Valid. After execution, \(x\) will be \(1\), satisfying the post-condition \(x = 1 \lor y = 2\).
Valid. The loop runs indefinitely, so the post-condition is vacuously true as the program never terminates.

Partial vs Total correctness

December 2, 2025

Definition. Hoare triple - total correctness [003z]

December 5, 2025

\[ [P]\ s\ [Q] \]

The total correctness Hoare triple asserts that:

\[ \sigma \vDash P \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \land \sigma ' \vDash Q \]

Or equivalently viewing the conditions as assertions on memory states:

\[ P(\sigma ) \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \land Q(\sigma ') \]

For the sake of completeness let's also show how we might implement this in lean:


  def TotalHoareTriple {P Q : Condition} (c : Stmt) : Prop :=
    ∀ σ, P σ → ∃ σ', (c, σ) ⇓ₛ σ' ∧ Q σ'

Quiz. Understanding hoare triples [0040]

December 5, 2025

What does \(\{\top \}\ s\ \{Q\}\) express?
What about \(\{P\}\ s\ \{\top \}\)?
What about \([P]\ s\ [\top ]\)?
When does \(\{\top \}\ s\ \{\bot \}\) hold?
When does \(\{\bot \}\ s\ \{Q\}\) hold?

Solution.

December 5, 2025

It states that no matter the initial state, if the program \(s\) terminates, then the postcondition \(Q\) will hold. In other words, all terminating states end up in or satisfy \(Q\).
It states that if the precondition \(P\) holds before execution of \(s\), then after execution (if it terminates), the postcondition will always be true. Since \(\top \) is always true, this Hoare triple is valid for any program \(s\) and precondition \(P\).
Since this is a total correctness Hoare triple, it states that if the precondition \(P\) holds before execution of \(s\), then the program \(s\) will always terminate, regardless of the final state. The postcondition \(\top \) is trivially satisfied since it is always true. In other words we terminate on all states satisfying \(P\).
This Hoare triple holds if and only if the program \(s\) never terminates for any initial state. Since the postcondition is \(\bot \), which is always false, the only way for the Hoare triple to be valid is if there are no terminating executions of \(s\).
This Hoare triple holds for any program \(s\) and postcondition \(Q\), because the precondition \(\bot \) is always false. Since there are no initial states that satisfy \(\bot \), the implication in the definition of the Hoare triple is vacuously true.

Inference rules

December 2, 2025

Definition. Inference Rule Schema - Hoare logic [0043]

December 5, 2025

To denote the idea of syntactic consequence / inference within Hoare logic we use the notation:

Which says that if we can derive the hoare triple \(\{P\}\ s_1\ \{Q\}\) and so on up to \(\{Q\}\ s_n\ \{R\}\) using the inference rules of Hoare logic, then we can derive the hoare triple \(\{P\}\ s\ \{R\}\).

Inference rules without any hypotheses are considered base cases.

Quiz. Hoare logic - assignment proof rule [0045]

December 5, 2025

Consider the assignment \(x := y\) and the postcondition \(x > 2\). What needs to hold before the assignment such that \(x > 2\) holds afterwards?
Consider \(i := i + 1\) and post-condition \(i > 10\). What do we need to know before the assignment such that i > 10 holds afterwards?

Solution.

December 5, 2025

Let's write this out first as a hoare triple: \(\{?\}\ x := y\ \{x > 2\}\). Without even looking at the assignment rule it should be obvious that if we want \(x > 2\) to hold after the assignment, then before the assignment we need \(y > 2\), since after the assignment \(x\) will take the value of \(y\). So the hoare triple is valid when we have: \(\{y > 2\}\ x := y\ \{x > 2\}\).
Similarly we write the hoare triple: \(\{?\}\ i := i + 1\ \{i > 10\}\). To ensure that \(i > 10\) holds after the assignment, we need to consider what value of \(i\) before the assignment will lead to \(i > 10\) afterwards. Since we are incrementing \(i\) by 1, we need \(i + 1 > 10\) before the assignment, so our hoare triple becomes \(\{i + 1 > 10\}\ i := i + 1 \{i > 10\}\).

Definition. Hoare triple inference rules - Nano language [0044]

December 5, 2025

The basic inference rules for the Hoare logic applied to the Nano language are as follows:

Quiz. A hypothetical proof rule [0046]

December 6, 2025

A friend suggests the following proof rule for assignments:

\[ \vdash \{(x = e) \to Q\}\ x := e\ \{Q\} \]

Is the proof rule correct?

Solution.

December 6, 2025

Now let's test out the rule on a particular hoare triple:

\[ \{?\}\ x := 4\ \{y = x\} \]

To make the hoare triple valid we would have to use the following precondition:

\[ \vdash \{(x = 4) \to y = x\}\ x := 4\ \{y = x\} \]

but let's now assume the following initial state:

\[ \sigma _1 = \{x \mapsto 3, y \mapsto 1\} \]

this does correctly entail our precondition, i.e. we have \(\sigma _1 \vDash P\) as necessary by virtue of vacous truth, then executing the statement we have:

\[ \langle x := 4, \sigma _1 \rangle \Downarrow \sigma _2 \]

In the new context clearly \(x\) is reassigned to 4, thus:

\[ \sigma _2 = \{x \mapsto 4, y \mapsto 1\} \]

But we can see that clearly \(\sigma _2\) violates our postcondition \(Q\), which is to say, \(\sigma _2 \nvDash (y = x)\). The implication of this is that while the hoare triple is derivable it is not then necessarily also valid, in words this proof rule is unsound.

For completeness let's also provide a proof of soundness. As a reminder soundness states that:

If a hoare triple is derivable using the inference rules of our system, then it is valid (i.e. true in all interpretations.)

Formally we express this as:

\[ \vdash \{P\}\ s\ \{Q\} \to \vDash \{P\}\ s\ \{Q\} \]

If we instantiate this rule for our hypothetical assignment rule we must demonstrate the following:

\[ \forall \sigma .\ \sigma \vDash (x = e) \to Q \land \exists \sigma '.\ \langle (x := e), \sigma \rangle \Downarrow \sigma ' \to \sigma ' \vDash Q \]

Proof.

December 6, 2025

Let \(\sigma \) be the initial state before the assignment \(x := e\). We must show that if \(\sigma \vDash (x = e) \to Q\), then, after executing \(x := e\), the resulting state \(\sigma '\) satisfies \(\sigma ' \vDash Q\) (i.e. is valid for the assertions in the postcondition).

Before the assignment we have \(\sigma \vDash (x = e) \to Q\), in other words this means that: \[ \sigma (x) = \sigma (e) \to \sigma \vDash Q \] so if the variable \(x\) in the initial state evaluates to the same thing as some expression \(e\) then our post postcondition is valid for this state.
After the assignment we have a new state \(\sigma '\) defined as: \[ \sigma '(x) = \sigma (e) \] with everything else being unchanged, which is to say that \[ \forall y.\ y\ \mathrlap {\,/}{=}\ x \land \sigma '(y) = \sigma (y) \]
Now we want to check if \(\sigma ' \vDash Q\) as desired, we proceed by a case analysis on the equality \(\sigma '(x) = \sigma (e)\)
- Case: \(\sigma (e) = \sigma (x)\), then by the precondition we have \(\sigma \vDash Q\). Since \(\sigma '\) only changes the value of \(x\) to \(\sigma (e)\), and \(Q\) is satisfied by the initial state \(\sigma \) it follows that \(\sigma ' \vDash Q\).
- Case: \(\sigma (e) \ \mathrlap {\,/}{=}\ \sigma (x)\), then our precondition becomes vacuously true as the antecedent is false. However, as the assignment does terminate we do need to ensure that \(Q\) holds in the new state \(\sigma '\). However, since \(Q\) can be arbitrary we cannot guarantee that \(\sigma ' \vDash Q\).

Let's link the proof of soundness back to the example, so in our inital state \(\sigma _1\) we have that:

\[ \sigma (x) \ \mathrlap {\,/}{=}\ \sigma (y) \equiv 3 \ \mathrlap {\,/}{=}\ 4 \]

Since this means that the equality \(x = 4\) is false we have that implication so the precondition \(P\) is true. This corresponds precisely to the second case where \(\sigma (e) \ \mathrlap {\,/}{=}\ \sigma (x)\). The issue we can then see which naturally follows is that in the new state clearly its the case that:

\[ \sigma _2 = \{x \mapsto 4, y \mapsto 1\} \nvDash (x = y) \]

In other words we had the case where our precondition was vacuously true thus erroneously implying upon termination the arbitrary \(y = x\) must also hold. Clearly then this proof rule is incorrect as in the case of a vacuous truth we are able to generate unsound hoare triples.

To compare this with the correct assignment rule we have:

\[ \vdash \{P[x \mapsto e]\}\ x := e\ \{P\} \]

we can notice here that by removing the consequent of the logical implication we ensure that if the assertion of x being substituted / being equal to the expression e before the execution of the statement doesn't hold, then it correctly means that we indeed cannot suggest that after an assignment our assertion \(P\) is somehow correct.

Quiz. Assessing provability [0047]

December 6, 2025

Using the correct proof rule for assignments, asses which of the hoare triples are provable i.e. valid.

\(\{y = 4\}\ x:= 4\ \{y = x\}\)
\(\{x + 1 = n\}\ x := x + 1\ \{x = n\}\)
\(\{y = x\}\ y := 2\ \{y = x\}\)
\(\{z = 3\}\ y := x\ \{z = 3\}\)

Solution.

December 6, 2025

Yes, since we have that for any state \(\sigma \) the substitution \[ (y = x)[x \mapsto 4] \] holds, thus our precondition holds and upon termination of the assignment clearly our postcondition then holds as well.
Yes, again we that our post condition says \(x = n\) so \((x = n)[ n \mapsto (x + 1)]\) holds as our precondition is then \[ (x + 1 = n)[n \mapsto (x + 1)] = (x + 1 = x + 1) \]
No, again using our reasoning we have \[ (y = x)[y \mapsto 2] = 2 = x \] but then if we have \(\sigma = \{ x \mapsto 3\}\) we can generate \[ \sigma \nvDash (2 = x) \equiv (2 = 3) \]
Yes, this is just correct by definition of a substitution leaving irrelevant variables unaffected.

Consequence

December 2, 2025

Definition. Precond. Strengthening & Postcond. Weakening [0048]

December 6, 2025

As a reminder in hoare logic we denote the consequence rule as follows:

On a high level this is quite evidently just transitivity, which is to say that if some assertion \(P'\) holds and by implication \(P\) holds, and upon successful termination of \(s\) we have that \(Q\) holds and by implication \(Q'\) holds, then we can transitively reason that \(\{P'\}\ s\ \{Q'\}\) would also hold for our program \(s\).

What we can do here is decompose this rule into two separate rules:

Precondition strengthening

December 6, 2025

The idea of strengthening here comes from the fact that the rhs of an implication always at least denotes a more restrictive or strengthened condition on the memory state \(\sigma \). So a basic example being clearly:

\[ x > 3 \to x > 2 \]

So if we have that:

\[ \sigma \vDash (x > 3) \to (x > 2) \\ \vdash \{x > 2\}\ s\ \{Q\} \]

Which is to say that our hoare triple is derivable under the weaker precondition \(x > 2\), then clearly the same hoare triple is also derivable under the stronger pre-condition \(x > 3\) as it implies our weaker condition, hence we can derive:

\[ \vdash \{x > 3\}\ s\ \{Q\} \]

An example program we could take here would be something like:

\[ \{x > 2\}\ \texttt {if}\ (x > 2)\ \texttt {then}\ y := 2 \texttt {else}\ y := 3\ \{y := 2\} \]

Clearly here the condition just requires that \(x\) is larger than 2, if our precondition asserts that its larger than 3, the \(\texttt {then}\) branch executes just the same and our postcondition holds.

Postcondition weakening

December 6, 2025

On a high level this says that if we can prove some postcondition \(Q'\), we can always relax this condition to something weaker. So in simpler terms if we have the fact that the postcondition \(Q'\) holds for some more restrictive state, then we can naturally lessen the restrictions and have it still hold.

Quiz. Postcondition Weakening examples [0049]

December 6, 2025

Suppose we can prove:

\[ \{\top \}\ s\ \{x = y \land z = 2\} \]

using the rule of post-condition weakening, which of the following can we prove?

\(\{\top \}\ s\ \{x = y\}\)
\(\{\top \}\ s \ \{z = 2\}\)
\(\{\top \}\ s\ \{z > 2\}\)
\(\{\top \}\ s\ \{\forall y.\ x = y\}\)
\(\{\top \}\ s\ \{\exists y.\ x = y\}\)

Solution.

December 6, 2025

Yes, this is provable, removing a conjunct is a common way of weakening an expresison as we are removing one condition.
Yes, this is provable, same reasoning as in (1)
This is also provable, more or less same reasoning as before, here we are using the fact that \[ z = 2 \to z > 0 \] since obviously \(2 > 0\)
No, this is not provable, while removing a conjunct does weaken our postcondition, if we then also quantify over all \(y\) we make an assertion which is stronger then what the conjunct says, i.e. that \(x = y\) for a specific \(y\), hence this is not provable.
Yes, this is provable. We have the fact that \[ a = b \equiv \exists a = b \] so clearly this is the same as what we did for (1) just with no desugaring of existential syntax

Definition. Hoare triple - partial correctness [003x]

December 5, 2025

The basic unit of reasoning or judgement of the partial correctness of a program is the Hoare triple denoted as:

\[ \{P\}\ s\ \{Q\} \]

where:

\(P\) represents the precondition which must hold true before the execution of the statement \(s\).
\(Q\) represents the postcondition which must hold true after the execution of the statement \(s\), provided that \(P\) was true before execution.

\[ \sigma \vDash P \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \to \sigma ' \vDash Q \]

\[ P(\sigma ) \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \to Q(\sigma ') \]

Or in lean equivalently as:


  abbrev Condition := Memory -> Prop

  def HoareTriple {P Q : Condition} (c : Stmt) : Prop :=
    ∀ σ σ', P σ → (c, σ) ⇓ₛ σ' → Q σ'

A note here is that we are using some custom notation for the big-step semantics relation. The notation \(\Downarrow _s\) here simply means the big step evaluation relation for statements.

In general for a Hoare triple we denote its validity as:

\[ \vDash \{P\}\ s\ \{Q\} \]