Definition. Weakest preconditions and Horn clauses [0056]

December 17, 2025

1. A motivating example

December 17, 2025

Let's consider the following Hoare triple:

\[ \vdash \{x > 0\}\ y := x;z := x + y\ \{z > 0\} \]

In order to prove that the triple is valid we would apply the rule of composition (or sequencing)

We know intuitively that what this means is we have to find an assertion \(r\) on the memory state such that

\[ \vdash \{x > 0\}\ y := x\ \{r(x, y, z)\} \land \vdash \{r(x, y, z)\}\ z := x + y\ \{z > 0\} \]

So the predicate / relation \(r\) represents some assertion over the variables in our state \(\sigma \). The natural question then becomes what is this predicate? The natural approach that could be taken here is to use the weakest precondition approach.

\[ \begin {align} \texttt {wp}(y := x,\ \texttt {wp}(z := x + y,\ z > 0)) &\equiv \\ \texttt {wp}(y := x,\ (z > 0)[z \mapsto x + y]) &\equiv \\ \texttt {wp}(y := x,\ x + y > 0) \end {align} \]

an equivalent way we can write this is

\[ \begin {align} \forall \sigma ,\sigma '.\ (x > 0 \land y = x)(\sigma ) \to (s_1, \sigma ) \Downarrow \sigma ' &\to q(x, y, z)(\sigma ') \\ \forall \sigma ,\sigma '.\ (q(x, y, z) \land z' = x + y) \to (s_2, \sigma ) \Downarrow \sigma ' &\to (z' > 0)(\sigma ) \end {align} \]

The important observation to make here is that if the Hoare triple is valid, we must have a solution for our relation \(q(x, y, z)\). Since our reasoning is furthermore predicated on the successful execution of the two statements, and we can implicitly assume we are reasoning over memory states let's simplify the above equations.

\[ \begin {align} (x > 0 \land y = x) &\to q(x, y, z) \\ (q(x, y, z) \land z' = x + y) &\to z' > 0 \end {align} \]

Now let's see if we can verify our earlier solution \(q(x, y, z) \triangleq x + y > 0\)

\[ \begin {align} x > 0 \land y = x &\to x + y > 0 \\ x + y > 0 \land z' = x + y &\to z' > 0 \end {align} \]

Clearly we can see both implications hold thus our earlier solution is indeed valid.

2. The rules

December 17, 2025

We'll enumerate the rules as a list:

For assignment: \[ \texttt {wp}(x := e, p(\overline x)) \triangleq p(\overline x)[x \mapsto e] \]
For sequential composition: \[ \texttt {wp}(s_1;s_2, p(\overline x)) \triangleq \texttt {wp}(s_1, \texttt {wp}(s_2, p(\overline x))) \]
For if statements: \[ \texttt {wp}(\texttt {if}\ b\texttt {then}\ s_1\ \texttt {else}\ s_2, p(\overline x)) \triangleq q(\overline x) \] with the constraints \[ \begin {align} q(\overline x) \land b &\to \texttt {wp}(s_1, p(\overline x)) \\ q(\overline x) \land \neg b &\to \texttt {wp}(s_2, p(\overline x)) \end {align} \]
For while loops: \[ \texttt {wp}(\texttt {while}\ b\ \texttt {do}\ s, p(\overline x)) \triangleq q(\overline x) \] with the constriants \[ \begin {align} q(\overline x) \land b &\to \texttt {wp}(s, q(\overline x)) \\ q(\overline x) \land \neg b &\to p(\overline x) \end {align} \]

Backlinks

Definition. Normalizing Horn clauses [0059]

December 19, 2025

Something of note when dealing with weakets preconditions in terms of horn clauses is that we have to first normalize them to ensure they are in the correct horn format, which is to say we commonly have some horn clause in the form

\[ p(e_1, e_2) \land \ldots \land \phi \to H(e_3) \]

where \(e_i\) represents an expression, to normalize these clauses we lift the expressions out of the parameters for the predicates and into the list of conjuncts, i.e.:

\[ p(x_1, x_2) \land x_1 = e_1 \land x_2 = e_2 \land x_3 = e_3 \land \ldots \land \phi \to H(x_3) \]

So we create fresh variables \(x_1, x_2, x_3\) and assign these to the respective expressions then use them in place of the expressions themselves.

Definition. Horn clauses - Syntax [004v]

December 15, 2025

A Horn clause is a disjunctive clause (disjunction of literals) with at most one positive, i.e. unnegated literal. Often written in implication form as a conjunction of literals implying some literal called the head.

\[ \underbrace {\underbrace {p(x_1, x_2) \land q(x_1, x_2, x_3) \land \ldots }_\text {queries} \land \underbrace {\phi }_\text {constraint}}_\text {body} \to \underbrace {H}_\text {head} \]

Here:

queries are relations over some vector of variables
\(\phi \) represents a formula in a first-order theory which does not contain queries
\(H\) is called the head and represents either a query in which case we also call the horn clause a definite class if it has the following shape \[ (p \land q \land \ldots \land \phi ) \to H \] or a fact if it has the following shape \[ \top \to H \] \(H\) can also be \(\bot \) in which case we refer to the horn clause as a gloal clause with the shape \[ (p \land q \land \ldots \land \phi ) \to \bot \] with the idea being that as opposed to assuming the query holds we now show that it holds

Free variables are implicitly universally quantified over, so a horn clause like

\[ \texttt {mortal}(X) \to \texttt {human}(X) \]

stands for

\[ \forall X.\ \texttt {mortal}(X) \to \texttt {human}(X) \]

Definition. Working backwards - weakest precondition [004k]

December 10, 2025

I'll split this explanation into 3 parts, first the basic intuition, then the pen-and-paper reasoning, and finally a more granular explanation.

The idea

December 10, 2025

Say we want to verify a hoare triple \(\{P\}\ s\ \{Q\}\), the weakest precondition approach is that we:

Start with our postcondition \(Q\) and, going backwards, we compute a formula \(\texttt {wp}(s, Q)\) called the weakest precondition of \(Q\) w.r.t the statement \(s\).
\(\texttt {wp}(s, Q)\) has the property that it's the weakest condition which guarantees that \(Q\) will hold after the termination of \(s\).

Therefore we can say that the triple is valid:

\[ \vDash \{P\}\ s\ \{Q\} \iff P \to \texttt {wp}(s, Q) \]

The basic rules

December 10, 2025

The basic rules can be recursively defined as follows:

For assignments: \[ \texttt {wp}(x := e, Q) \triangleq Q[x \mapsto e] \]
For composition \[ \texttt {wp}(s_1; s_2, Q) \triangleq \texttt {wp}(s_1, \texttt {wp}(s_2, Q)) \]
For conditionals \[ \texttt {wp}(\texttt {if}\ b\ \texttt {then}\ s_1\ \texttt {else}\ s_2, Q) \triangleq (b \to \texttt {wp}(s_1, Q)) \land (\neg b \to \texttt {wp}(s_2, Q)) \]

The more detailed reasoning

December 10, 2025

As a reminder, a Hoare triple:

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

Is simply a kind of syntax sugar for the logical formula:

\[ \forall \sigma , \sigma '.\ P(\sigma ) \to (s, \sigma ) \Downarrow \sigma ' \to Q(\sigma ) \]

So for all source and target states, if we terminate on \(s\) then \(Q\) holds. Additionally, for different kinds of expressions we also have our constructions rules to ensure soundness, take for example assignment, our rule to only derive valid Hoare triples was:

If we assume \(e\) to be some variable expression in a context \(\sigma : \texttt {Vars} \to \mathbb {Z}\) which has to evaluate to a number before assignment then we can write the above rule more pedantically as:

\[ \forall \sigma , \sigma '.\ (\forall n : \mathbb {Z}.\ (e, \sigma ) \Downarrow n \to Q[x \mapsto n]) \to (x := e, \sigma ) \Downarrow \sigma ' \to Q(\sigma ') \]

The idea of backwards reasoning here is as follows:

First we look at the big step evaluation \((x := e, \sigma ) \Downarrow \sigma '\), we know that if this assignment succeeded, it implies there must have been a successful evaluation of the \(e\) term, we know this because the only way to have derived this step is by the following inference rule:
Using what we've learned from (1) we apply the notion of inversion, i.e. if we know a conclusion to be true, we can assert the premises of that conclusion must have also been true, this in a sense gives us the premises to use as new judgements.
Now looking at the expression \[ \forall n : \mathbb {Z},.\ (e, \sigma ) \Downarrow n \to Q[x \mapsto n] \] we can clearly derive the precondition \(Q[x \mapsto n]\) since we know the antecedent \(\forall n.\ (e, \sigma ) \Downarrow n\) is true, as it must have been true to derive the big step evaluation.
Since we have now demonstrated we can indeed provide sufficient reasoning to arrive at our conclusion \(Q(\sigma ')\) this finishes the proof.

The shorthand of the weakest precondition is nothing more than an expression of precisely this idea in a more concise fashion. Take for example \(\texttt {if conditions}\).

We again start from our post-condition then proceed with a case split or more accurately an inversion on the evaluation rule.
The inversion naturally gives us two branches, the true and false branch. This represents the conjunction here, then with each conjunct the antecedent of the implication is represented by the true or false guard condition \(b\), the consequent in this instance is simply a recursive call on the \(\texttt {then}\) and \(\texttt {else}\) branch bodies.

The main thing I'm trying to drive home here is that the weakest precondition idea is fundamentally just based on the concept of:

Seeing how a term must have been derived
Recursively going up the chain of any other sub-terms

So in a straightforward way, it's nothing more than chaining together all the individual proof rules for the various hoare triples. To show an example in lean using a some nice macros to create a simple syntax:


    example (n : Num) : 
    {{ ⟦ "x" ↦ n ⟧ }} 
      tm{ x := x + 1 } 
    {{ ⟦ "x" ↦ n + 1 ⟧ }} := by
    apply Hoare.assign'
    intro σ m hpre heval
    cases heval with
    | sum he1 he2 =>
      cases he1; cases he2
      simp [hpre]

The hoare triple we are proving here corresponds to this in the normal syntax:

\[ \{x \mapsto n \}\ x := x + 1\ \{x \mapsto n + 1\} \]

We can see here to "prove" this hoare triple was valid we started by doing our standard case split on the assign - that's the \(\texttt {apply Hoare.assign'}\) - statement, then we were inside the addition, here we did a case split which gave us the lhs and rhs we were adding, after doing a case split on those two sides we could finally just simplify (and finalize) our proof using the fact that in \(\sigma \) \(x\) evaluates to \(n\).