Definition. Theory of Arrays [003l]

December 2, 2025

The theory of arrays is a first-order theory that models arrays as functions from indices to values. Its signature includes:

\[ \Sigma _A \triangleq \{- [ - ], \langle - \triangleleft - \rangle , =\} \]

where:

\(-[ - ]\): read operation, which takes an array and an index and returns the value at that index.
\(\langle - \triangleleft - \rangle \): write operation, which takes an array, an index, and a value, and returns a new array with the value at the specified index updated.
\(=\): equality relation, which checks if two arrays are identical.

The axioms of the theory of arrays are:

Context

VU-VFS-2025. Lecture 6 - Hoare logic & Weakest preconditions [004a]

December 6, 2025

Loops & Invariants

December 6, 2025

Quiz. Checking valid invariants [004c]

December 6, 2025

Consider the following code:


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

Which of the following is a loop invariant?

\(i \leq n\)
\(i < n\)
\(j \geq n\)

Solution.

December 6, 2025

Before the loop \(i = 0\) and \(n = 10\), since that means \(i \leq n\) is true we move on to checking it holds true after each loop iteration. What we can observe is that the loop condition is \(i < n\) and during the loop we have \(i = i + 1\), what this suggests is that clearly during the iteratons the invariant holds, additionally when \(i = 10\) we have that \(10 < 0 \to \bot \) hence the invariant also holds upon the termination of the loop, i.e. after the final iteration, thus it's indeed a valid loop invariant.
No, this is not a valid invariant, we can see that its very close to being right, but it doesnt account for the case after the final iteration and before we check the loop condition, i.e. where \(i = 10\), hence its not a valid loop invariant because it does not hold true after each iteration.
No, this is quite easy to see as it immediately fails even before we get into the loop as \(0 \geq 10 \to \bot \).

Quiz. Proving validity with invariants [004d]

December 6, 2025

Let's consider the statement \(W\):


  while x < n do 
    x = x + 1

Answer the following questions:

Prove the validity of \[ \vdash \{x \leq n\}\ W\ \{x \geq n\} \] using the loop invariant \(I = x \leq n\)
Would \(\top \) also have worked as a loop invariant?
If we changed the post condition to \(x = n\), what would that have changed?

Solution.

December 6, 2025

As the usual piece of little assistance let's take a look at the while rule

Here we can try to construct the proof tree first of all, instantiating our rule with the given invariant we have: Using the assignment rule we then want to prove the antecident here, so instantiating this with or postcondition \(Q\) we have in other words our precondition becomes \[ (x + 1) \leq n \] Therefore the use the assignment rule we want we have to demonstrate \[ (x \leq n \land x < n \to (x + 1) \leq n) \] since we have that \[ x \leq n \land x < n \equiv x < n \to (x + 1) \leq n \] we clearly have that
Yes, let's again instantiate our rule since our postcondition for the assignmnet is a tautology, i.e. always valid, it will hold under substitution thus making the assignment trivially valid hence working as a correct loop invariant.
Something we could observe in question (1) is that so this is a bit of a trick question in that with question 1 we are actually just using a postcondition weaking on this postcondition, hence this is naturally a valid postcondition.

Definition. Invariant [004f]

December 7, 2025

In the most straightforward sense we say that an invariant is simply:

A property that holds at all reachable states of the program

Formally we can say if \(P\) denotes our property and \(\mathcal R\) denotes our set of reachable states then we can say that \(P\) is an invariant if:

\[ \forall \sigma , \sigma \in \mathcal R \to P(\sigma ) \]

An important thing to note here is that an invariant by itself does not need to be checkable or syntactic in any sense, there are no requirements that \(P\) must imply after each step. The distinction here is important because we can have something be an invariant though be insufficient as a proof rule.

Definition. Inductive Invariant [004e]

December 6, 2025

An inductive invariant is a regular invariant, which is to say that it:

is a property which holds at all reachable states of the program

But it has the additional constraint that it must be closed under the transition relation. In other words if it holds before a step, it must also hold after the step. Formally we say that a property \(P\) represents an inductive invariant if:

As a base case it holds at program initialization \[ \texttt {init} \to P \]
In the inductive step we have \[ P(\sigma ) \land (S, \sigma ) \to \sigma ' \to P(\sigma ') \] in plain English: If the property holds on the state \(\sigma \) and after the small step evaluation \(S\) we land in a new state \(\sigma '\) then the property also holds in the new state \(\sigma '\).

If both of the conditions hold then we we automatically have that:

\[ \sigma \in \mathcal R.\ P(\sigma ) \]

Which is to say that these conditions imply an inductive invariant is also an invariant. The prime example where we can see this is in the case of the while loop for hoare logic:

Here the invariant is represented by the assertion \(I\) on the memory state. What this rule says is that:

If the assertion \(I\) and the loop guard \(b\) hold, and upon termination of \(s\) we have that \(I\) holds.
Then we can lift the invariant out of the loop and say that it must hold for all loop iterations and upon termination of the loop we clearly have that our loop guard must be false and our invariant should still hold.

This corresponds precisely to the notion of an inductive invariant as if we can demonstrate it holding for the execution and termination of a single statement - the base case - then we can derive the inductive case where it holds for all iterations.

Quiz. Finding inductive invariants [004g]

December 7, 2025

Consider the following statement \(W\):


  while x < n do
    x := y;
    y := x + 1

Say that we wanted to prove the following Hoare triple:

\[ \{x = 0 \land y = 1\}\ W\ \{x \geq 0\} \]

What is an inductive invariant \(I\) which allows us to prove the triple?

Solution.

December 7, 2025

For reference lets pull up the while rule again:

One not entirely unreasonable albiet simple choice is to try out the post condition \(x \geq 0\), its not too uncommon that a valid postcondition - or more often a variant of it - are in fact valid loop invariants. Testing this out it means we would have to prove the body:

\[ \vdash \{x \geq 0 \land x < n\}\ x := y; y := x + 1\ \{x \geq 0\} \]

To see if this is inductive we can try and find a counterexample to demonstrate its not, and indeed we can see that \(\sigma = \{y \mapsto -1000, x \mapsto 1, n \mapsto 2 \}\) would mean that \(P(\sigma )\) would hold, and we could indeed step to a state \(\sigma '\) though clearly we have that:

\[ \sigma ' \ \mathrlap {\,/}{\vDash }\ (x \geq 0)[x \mapsto -1000] \]

Since we can see here that the unconstrained \(y\) is causing is issues lets go with:

\[ I \triangleq x \geq 0 \land y = x + 1 \]

Since this ensures that \(y\) is correctly related to \(x\) it means that we indeed have that \[ \sigma \vDash I (x := y; y := x + 1, \sigma ) \to \sigma ' \to \sigma ' \vDash I \] as desired

Arrays & Invariants

December 6, 2025

Definition. Theory of Arrays [003l]

December 2, 2025

The theory of arrays is a first-order theory that models arrays as functions from indices to values. Its signature includes:

\[ \Sigma _A \triangleq \{- [ - ], \langle - \triangleleft - \rangle , =\} \]

where:

\(-[ - ]\): read operation, which takes an array and an index and returns the value at that index.
\(\langle - \triangleleft - \rangle \): write operation, which takes an array, an index, and a value, and returns a new array with the value at the specified index updated.
\(=\): equality relation, which checks if two arrays are identical.

The axioms of the theory of arrays are:

Quiz. A hypothetical array inference rule [004i]

December 7, 2025

Say we want to add arrays to our programming language, and we come up with the following inference rule to reason about assignments:

Is this rule correct?

Solution.

December 7, 2025

There are a few ways we can answer this, starting in with the most pedantic let's construct the proof tree and then see if we can come up with a counter example, we consider the following hoare triple:

\[ \{i = 1\}\ a[i] := 3; a[1] := 2\ \{a[i] = 3\} \]

By the sequence and precondition strengthening rule we have that

Of note here we are deriving \(i = 1\) through the following implications:

\[ Q[a[i] \mapsto 3] \equiv (a[i] = 3)[a[i] \mapsto 3] \equiv (3 = 3) \equiv \top \]

Where we know that \(i = 1 \to \top \) so we can use precondition strengthening to use \(i = 1\) as our precondition since it implies something we've already syntactically demonstrated to be provable.

Clearly we have that the first assignment in the sequence holds by the naive assignment, same for the second assignment \(a[1] = 2\) since it precondition reduces to the tautology \(\top \), so the final rule is then derivable. But we can obviously see that it erroneously assumes that \(i\) represents some kind of distinct index but, we can see that in the second assignment its aliased by the constant index \(1\) which means that while we can derive the rule it is not semantically valid hence unsound.

To compare this with the correct rule we have that:

Now again let's try to derive the hoare triple we want to prove correct:

To derive we want to find some assertion \(R\), applying the correct assignment rule to the second assignment we define \(R\) as.

\[ R \equiv (a[i] := 3)[a \mapsto a \langle 1 \lhd 2 \rangle ] \]

we can think of this as defining the function:

\[ a'(j) = \begin {cases} 2 & \texttt {if}\ j = 1 \\ a(j) & \text {otherwise} \end {cases} \]

we can then do a case split on the equality \(i = 1\) using our defined function

If \(i = 1\) then we have \[ a'[i] = a[1] = 2 \to a'[i] = 3 \equiv 2 = 3 \equiv \bot \]
If \(i \ \mathrlap {\,/}{=}\ 1\) we have \[ a'[i] = a[i] \to a'[i] = 3 \equiv a[i] = 3 \]

Since it clearly must be the case that \(i \ \mathrlap {\,/}{=}\ 1\) it implies that our assertion \(R\) is equivalent to:

\[ R \equiv (i \ \mathrlap {\,/}{=}\ 1\land a[i] = 3) \]

Now testing this rule on the first hoare triple:

\[ \{i = 1\}\ a[i] := 3\ \{i \ \mathrlap {\,/}{=}\ 1\land a[i] = 3\} \]

By the assignment rule we must somehow be able to derive \(i = 1\) from the following:

\[ R[a \mapsto a \langle i \lhd 3 \rangle ] \]

substituting in our \(R\) we get

\[ (i \ \mathrlap {\,/}{=}\ 1\land a[i] = 3)[a \mapsto a \langle i \lhd 3 \rangle ] \]

after a reduction we have

\[ (i \ \mathrlap {\,/}{=}\ 1 \land \underbrace {(a \langle i \lhd 3 \rangle [i] = 3)}_{\top }) \]

simplifying this we get

\[ (i \ \mathrlap {\,/}{=}\ 1) \]

Which is where the crux of our issue lies, the precondition of our Hoare triple was \(i = 1\), but clearly here to derive our sequence of assignments we must have that i is not 1, hence this hoare triple is not derivable as its also clearly not valid.

A simpler approach at establishing the same idea is by just directly working backwards

\[ \begin {align} a \langle 1 \lhd 2 \rangle [i] & = 3 \\ a \langle i \lhd 3 \rangle \langle 1 \lhd 2 \rangle [i] & = 3 \end {align} \]

so first we substitute \(a\) for the assignment \(a[1] := 2\), then we update it for the assignment \(a[i] := 3\), then our precondition would imply that:

\[ i = 1 \to a \langle i \lhd 3 \rangle \langle 1 \lhd 2 \rangle [i] = 3 \]

We indeed cannot derive the triple with the precondition, as it should be trivially apparent that if \(i = 1\) after overwriting with \(a[1] = 2\) we clearly cannot have \(a[1] = 3\).

Quiz. Theory of arrays \(T_A\) [003m]

December 2, 2025

Which of the following formula is valid/satisfiable/unsatisfiable ?

\(a[3] = 2\)
\(a \langle 3 \triangleleft 5 \rangle [3] = 5\)
\(a \langle 3 \triangleleft 5 \rangle [3] = 3\)
\(a[3] = 2\land a \langle 3 \triangleleft 5 \rangle [3] = 5\)

Solution.

December 2, 2025

This formula is satisfiable. For example, if we have an array \(a\) such that \(a[3] = 2\), then the formula holds true.
This formula is valid. According to the Read-Over-Write axiom, when we write a value to an index in an array and then read from that same index, we get the value we just wrote. So regardless of the initial contents of array \(a\), after performing the write operation \(a \langle 3 \triangleleft 5 \rangle \), reading from index \(3\) will always yield \(5\) hence making it always true (valid).
This formula is unsatisfiable. According to the Read-Over-Write axiom, when we write a value to an index in an array and then read from that same index, we get the value we just wrote. Therefore, after performing the write operation \(a \langle 3 \triangleleft 5 \rangle \), reading from index \(3\) will always yield \(5\), making it impossible for it to equal \(3\).
This formula is satisfiable. For example, if we have an array \(a\) such that \(a[3] = 2\), then after performing the write operation \(a \langle 3 \triangleleft 5 \rangle \), reading from index \(3\) will yield \(5\). Thus, both parts of the conjunction can be true simultaneously though are not valid in all interpretations.

Quiz. Finding inductive invariants - arrays [004j]

December 10, 2025

Consider the following while loop \(W\):


  while i < n do
    a[i] := 0;
    i    := i + 1

Consider the following pre-and-post condition:

\[ \{i = 0 \land n > 0\}\ W\ \{\forall j.\ 0 \leq j < n \to a[j] = 0\} \]

What is an inductive invariant that shows correctness?

Solution.

December 10, 2025

This is almost a sort of canonical example where the index replacement trick works really nicely. On a high level our postcondition asserts something about the array over the first \(n\) indices, hence if we want to have an invariant which shows correctness, we can simply reframe our postcondition as an assertion up to the \(i\)th position / iteration, in other words we simply replace \(n\) with \(i\):

\[ \forall j.\ 0 \leq j < i \to a[j] = 0 \]

Soundness & Completeness

December 6, 2025

Definition. Soundness & Completeness - Hoare triples [0041]

December 5, 2025

In a very general sense if we have a logical or formal system a core idea is that we only want to prove things that are actually true, and conversely if we find something that is true we would want to be able to prove it. This leads to two important properties of formal systems:

Soundness is the property that everything provable within the system is in fact true, within the context of hoare logic it means that all hoare triples which we can syntactically derive using our inference rules are by implication valid (i.e. true in all interpretations), formally: \[ \vdash \{P\}\ s\ \{Q\} \to \ \vDash \{P\}\ s\ \{Q\} \]
Completeness is the property that everything that is true can be proven within the system, in the context of hoare logic it means that all valid hoare triples can be syntactically derived using our inference rules, formally: \[ \vDash \{P\}\ s\ \{Q\} \to \ \vdash \{P\}\ s\ \{Q\} \]

Weakest precondition

December 6, 2025

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\).

Definition. Weakest precondition - while loop [004m]

December 10, 2025

In an abstract sense the weakest precondition for while loops is no different from that for most other syntactic constructs, to reason backward we apply inversion to the statement we are considering; in this case the while loop; and then simply recurse on the sub-terms. Though the while loop differentiates itself through the notion of invariants.

Before we define how to compute the weakest precondition let's define the hoare rule again:

The central thing to observe here is the invariant hypothesis which acts as the premise for the while loop formation, if we write expand it out a bit we get:

\[ \{I(\sigma ) \land b \Downarrow ^t \sigma \}\ s\ \{I\} \]

So the idea, to reiterate again, is that if our invariant holds in the state \(\sigma \) and our loop condition evaluates to \(\texttt {true}\), then upon termination of \(s\) i.e. the loop body we have that the invariant \(I\) still holds.

In the false case our proof becomes trivial through inversion we know there is some terminating state \(\sigma _t\) and we know the loop condition must have evaluated to false, hence we can immediately provide the conditions to fulfill the postcondition and thus create our valid hoare triple.
The true case is a bit more complex, first let's look at the evaluation semantics for it We can see the final state is \(\sigma _3\) this means that the post-condition we want to prove for the true state is \[ I(\sigma _3) \land b \Downarrow ^f \sigma _3 \] The main thing we leverage here is the invariant hypothesis, rewriting it as a function we have \[ \lambda (\sigma , \sigma ').\ \lambda ( I(\sigma ) \land b \Downarrow ^f \sigma ).\ \lambda ((c, \sigma ) \Downarrow \sigma ').\ I(\sigma ') \] in addition to \[ \lambda \sigma .\ \lambda I(\sigma ).\ \lambda (\langle W, \sigma \rangle = \langle W, \sigma _2 \rangle ).\ I(\sigma _3) \land b \Downarrow ^f \sigma _3 \] The idea is then that we use inversion to give us the evaluated terms, we plug those terms into the invariant hypothesis to get \(I(\sigma _2)\), then using \(\sigma _2\), \(I(\sigma _2)\), and reflexivity (since \(\langle W, \sigma _2\rangle \equiv \langle W, \sigma _2 \rangle \)) we have created the proof that the invariant holds for the final memory state and the loop guard indeed evaluates to false.

Quiz. Computing weakest preconditions [004l]

December 10, 2025

Consider the following statement:


  x := y + 1;
  if x > 0 then
    z := 1
  else
    z := -1

Answer the following questions:

What is \(\texttt {wp}(s, z > 0)\)
What is \(\texttt {wp}(s, z \leq 0)\)
Can we prove \(\{-1 \leq y\}\ s\ \{z > 0\}\)
What about \(\{y > -1\}\ s\ \{z > 0\}\)

Solution.

December 10, 2025

In an abstract sense the statement is a sequence of an assignment and an if statement, starting with the if statement we get: \[ (x > 0) \to \texttt {wp}(z := 1, Q) \land (x \leq 0) \to \texttt {wp}(z := -1, Q) \] Both of the assignments resolve to substitutions of 1 and -1, so we get \[ (x > 0) \to (z > 0)[z \mapsto 1] \land (x \leq 0) \to (z > 0)[z \mapsto -1] \] With sequences we know it's a nested pattern, i.e. \(\texttt {wp}(s_1, \texttt {wp}(s_2, Q))\), the second argument we already have, we know that \(s_1\) here is just the assignment, so again we apply the subtitution \[ ((x > 0) \to Q[z \mapsto 1] \land (x \leq 0) \to Q[z \mapsto -1])[x \mapsto (y + 1)] \] which reduces to \[ \begin {align} ((y + 1 > 0) \to (1 > 0) &\land (y + 1 \leq 0) \to (-1 > 0)) \\ ((y + 1 > 0) \to \top &\land (y + 1 \leq 0) \to \bot ) \\ ((y + 1 > 0) \to \top &\land \neg (y + 1 \leq 0)) \\ ((y + 1 > 0) \to \top &\land (y + 1 > 0)) \\ ((y + 1 > 0) \to \top )& \\ (y + 1 > 0)& \\ \end {align} \]
To skip ahead a slight bit, so we have \[ (x > 0) \to (z \leq 0)[z \mapsto 1] \land (x \leq 0) \to (z \leq 0)[z \mapsto -1] \] then substituting for the intial assignment of \(x\) \[ (y + 1 > 0) \to (1 \leq 0) \land (y + 1 \leq 0) \to (-1 \leq 0) \] Here we just end up in the reverse case, i.e. \[ (y + 1 > 0) \to (\bot ) \land (y + 1 \leq 0) \to \top \] reduces now to \[ (y + 1 \leq 0) \]
The high level idea here is that we computed the weakest precondition for \(z > 0\) already, it was \[ (y + 1 > 0) \] since it's the weakest we can only admit other preconditions if they imply the weakest one, so if we then look at the implication \[ -1 > y \to (y + 1 > 0) \] we can trivially see that this implication does not hold, i.e. we cannot apply precondition strengthening here hence the rule does not allow us to prove the hoare triple.
Same reasoning as above, but now it works since \[ y > -1 \to y + 1 > 0 \] indeed makes sense

Example. Verification conditions in while loops [004n]

December 11, 2025

Let's consider the following while loop:


  @pre x <= 0
  while [x <= 6] (x <= 5) do
    x := x + 1
  @post x = 6

if we denote the loop and its body as \(W\), then it corresponds to the following hoare triple:

\[ \{x \leq 0\}\ W\ \{x = 6\} \]

With the addition of the invariant \(I \triangleq x \leq 6\), now the verification condition for the loop is expressed as:

\[ \begin {align} \texttt {vc}(W [I], x = 6) &= \forall \sigma .\ I(\sigma ) \land (b \Downarrow ^t \sigma ) \to \texttt {wp}(W [I], s, I(\sigma )) \\ &\land \forall \sigma .\ I(\sigma ) \land (b \Downarrow ^f \sigma ) \to Q(\sigma ) \\ &\land \texttt {vc}(s, I) \end {align} \]

starting with the first conjunct with have:

\[ \forall \sigma , x \leq 6 \to (x \leq 5 \Downarrow ^t \sigma ) \to \texttt {wp}(x := x + 1, (x \leq 6)) \]

After we unfold the \(\texttt {wp}\) our goal reduces to:

\[ x \mapsto x + 1 \leq 6 \equiv x \leq 5 \]

And we clearly know this is true just by inversion of the evaluation of the loop guard. Moving on to the second conjunct:

\[ \forall \sigma .\ x \leq 6 \land (x \leq 5 \Downarrow ^f \sigma ) \to x = 6 \]

This represents our termination condition, here we know by inversion of the loop guard again that the premise of our implication becomes:

\[ x \leq 6 \land x > 5 \to x = 6 \]

Our final conjunct is the verification condition on the assignment, so:

\[ \texttt {vc}(x := x + 1, x \leq 6) \]

Unfolding the call again we know this just resolves to \(\top \) as there are no verification conditions for assignment.

Finally we also have to demonstrate that:

\[ (x \leq 0 \land x = x_0) \to \texttt {wp}(W [I], Q) \]

unfolding the \(\texttt {wp}\) again gives

\[ (x \leq 0 \land x = x_0) \to x \leq 6 \]

Clearly we can see this trivially holds, i.e. our precondition is stronger than the invariant, hence by precondition strengthening, it is valid.

How do we get there though?

December 11, 2025

I do think it's worth telling this as a bit of a story, we start with the fundamental theorem for while loops:

So this is just the expanded rule for constructing valid or sound while hoare triples, now this rule assumes that the invariant \(I\) is the same as the precondition \(P\) which is naturally not always the case, so it could be nice to have a rule which accounts for constructing valid while loops with invariants and custom preconditions. Same with custom post-conditions \(Q\).

If you want to be super pedantic you could show how this is just a combination of consequence + while rule. Anyway then, moving on we have the rule for \(\texttt {wp}\) soundness.

Now depending on how you actually design your \(\texttt {wp}\) and \(\texttt {vc}\) code this rule can look slightly different, though I like this distinction, in this instance for the case of while loops \(\texttt {wp}(W[I], Q)\) simply returns the invariant \(I\), this means that again if we want to have a custom precondition for \(W\) we'd want to verify we would extend the rule as:

Thus for while loops it would become:

Where the verification conditions would unfold to what we discussed before.

A nice point to make here is that all of these rules are essentially derived from one another, which is to say that:

In a conceptual sense verification conditions i.e. what we need to prove to demonstrate a hoare triple is valid, are simply a convenience mechanism derived from the fundamental logic of how we construct a hoare triple.

VU-VFS-2025. Lecture 4 - First Order Theories [0032]

December 2, 2025

Signatures and Axioms

December 2, 2025

Definition. First Order Theory \(T\) [0033]

December 2, 2025

A first order theory (FOT) \(T\) is defined by two main components:

A signature \(\Sigma \) of a set of constant, function, and predicate symbols
A set of axioms \(\mathcal A\) consisting of closed (i.e. no free variables) formulas over the signature \(\Sigma \)

We say that a formula constructed from only from the contents of the signature \(\Sigma \) is a \(\Sigma \)-formula.

Quiz. Signatures and Axioms (FOL) [0034]

December 2, 2025

Consider a theory withthe following signature:

\[ \Sigma _H : \{R = \{\texttt {taller}\}, C = F = \emptyset \} \]

And the axiom:

\[ \forall x.\ \forall y.\ (\texttt {taller}(x, y) \to \neg \texttt {taller}(y, x)) \]

Are the following legal \(\Sigma _H\)-formulas?

\( \exists x.\ \forall y.\ (\texttt {taller}(x, z) \land \texttt {taller}(y, w)) \)
\( \exists x.\ \forall z.\ \texttt {taller}(x, z) \land \texttt {taller}(\text {joe}, \text {tom}) \)

Solution.

December 2, 2025

Yes
No, there are no constants in the signature, so \text {joe} and \text {tom} are not valid terms.

Models of Theories

December 2, 2025

Definition. Structure & Model of \(T\) (FOT) [0035]

December 2, 2025

A structure which we denote as:

\[ M \triangleq \langle U, I \rangle \]

Is a model of a theory \(T\) (or \(T\)-model) iff:

\[ \forall A \in \mathcal A_T.\ M \vDash A \]

where:

\(U\) is the universe or more commonly the domain
\(I\) is the interpretation which assigns some meaning to our formula

Quiz. Models of \(T_H\) [0036]

December 2, 2025

consider a structure consisting of a universe \(U\) and interpretation \(I\) as follows:

\[ U = \{A, B\} \quad I = \{\texttt {taller} \mapsto \{\langle A, A\rangle , \langle B, B\rangle \}\} \]

Are the following models of the theory \(T\) or not:

Is \(\langle U, I\rangle \) a model of \(T\)
If we change the interpretation to \[ I = \{\texttt {taller} \mapsto \{\langle A, B\rangle \}\} \] is the structure now a model of \(T\)?
If we add the following axiom \[ \forall x, y, z.\ (\texttt {taller}(x, y) \land \texttt {taller}(y, z) \to \texttt {taller}(x, z)) \] and we change the interpretation to \[ I = \{\texttt {taller} \mapsto \{\langle A, B \rangle , \langle B, C \rangle \}\} \] then is the structure a model of \(T\)?

Solution.

December 2, 2025

As a reminder we are working with the axiom:

\[ \forall x, y.\ (\texttt {taller}(x, y) \to \neg \texttt {taller}(y, x)) \]

Clearly no, as if we take \(x = A\) and \(y = A\) we have that both \(\texttt {taller}(A, A)\) and \(\texttt {taller}(A, A)\) hold, violating the axiom.
Here we are chaning or interpretation to just the relation \(\texttt {taller}(A, B)\) holding. In this case the axiom is satisfied as there are no values of \(x\) and \(y\) such that both \(\texttt {taller}(x, y)\) and \(\texttt {taller}(y, x)\) hold. So yes this is a model of \(T\).
No, as if we take \(x = A\), \(y = B\) and \(z = C\) we have that both \(\texttt {taller}(A, B)\) and \(\texttt {taller}(B, C)\) hold, but \(\texttt {taller}(A, C)\) does not hold (so not in our interpretation for the \(\texttt {taller}\) relationship), violating the axiom.

Satisfiability Modulo \(T\)

December 2, 2025

Definition. Satisfiable & Valid modulo \(T\) [0037]

December 2, 2025

We say that a formula \(F\) is satisfiable modulo \(T\) iff there exists a \(T\)-model \(M\) and a variable assignment \(\sigma \) such that:

\[ M, \sigma \vDash F \]

We say that a formula \(F\) is valid modulo \(T\) iff forall \(T\)-models \(M\) and all variable assignments \(\sigma \) we have:

\[ M, \sigma \vDash F \]

Definition. FOL Validity vs Valid modulo \(T\) [0039]

December 2, 2025

We can compare the two notions by understanding validity in modulo \(T\) as a restriction of validity in FOL to only those models that are \(T\)-models. So the implication of that is that if a formula is valid (true in all models), then its clearly also valid in the subset/restriction to only \(T\)-models. However, the other way around does not hold, since a formula can be true in all \(T\)-models, but false in some non-\(T\)-model. Hence we have the following:

But the other way around does not hold in general:

Quiz. Satisfiability in FOL vs FOT [0038]

December 2, 2025

Consider some arbitrary first order theory \(T\)

If a formula is valid in FOL, then is it also valid in modulo \(T\)?
If a formula is valid modulo \(T\), then is it also valid in FOL?

Solution.

December 2, 2025

Yes, if its valid in FOL that means its valid in all models which includes those models that are \(T\)-models. Hence its also valid modulo \(T\).
No, a formula can be valid in all \(T\)-models, but false in some non-\(T\)-model. Hence its not necessarily valid in FOL.

Theory of Equality & Congruence

December 2, 2025

Definition. Theory of Equality \(T\) [003a]

December 2, 2025

The theory of equality \(T_=\) is a first order theory over the signature \(\Sigma _=\) which contains:

\[ \sigma _= : \{=, s\} \]

Where \(=\) is a binary relation symbol and \(s\) is any constant function or predicate symbol. The axioms of the theory of equality are:

Quiz. Theory of Equality [003b]

December 2, 2025

Consider the universe:

\[ U = \{\alpha , \beta \} \]

which of the following interpetations of \(=\) are allowd by the axioms of \(T_=\):

\(I(=) \triangleq \{\langle \alpha , \beta \rangle , \langle \beta \alpha \rangle \}\)
\(I(=) \triangleq \{\langle \alpha , \alpha \rangle , \langle \beta , \beta \rangle \}\)
\(I(=) \triangleq \{\langle \alpha , \alpha \rangle , \langle \alpha , \beta \rangle , \langle \beta , \alpha \rangle , \langle \beta , \beta \rangle \}\)

Solution.

December 2, 2025

No, violates reflexivity axiom since neither \(\alpha = \alpha \) nor \(\beta = \beta \) are in the interpretation
Yes, satisfies all axioms of equality
Yes, satisfies all axioms of equality

Definition. (Left & Right) Congruence Relations (FOT) [003c]

December 2, 2025

In the most general sense we say that a relation \(R\) over a set \(A\) is a congruence with respect to a function \(f : A^n \to A\) if for all \(a_1, \ldots , a_n, b_1, \ldots , b_n \in A\) such that \(a_i\ R\ b_i\) for all \(1 \leq i \leq n\) we have:

\[ f(a_1, \ldots , a_n)\ R\ f(b_1, \ldots , b_n) \]

if we denote \(\overline x\) as a vector of elements \(x_1, \ldots , x_n\) we can rewrite this more succinctly as:

\[ \forall \overline a, \overline b \in A^n.\ (\forall i.\ a_i\ R\ b_i) \to f(\overline a)\ R\ f(\overline b) \]

In the case of first order theories we can then instantiate \(R\) with things like equality or other relations defined in the theory. Additionally we can \(f\) represent a function or predicate symbol from the signature of the theory. In the case of binary functions or predicates we can also define left and right congruence as follows:

A relation \(R\) is a left congruence with respect to a binary function or predicate \(f : A \times A \to A\) if for all \(a, b, c \in A\) such that \(a\ R\ b\) we have:
A relation \(R\) is a right congruence with respect to a binary function or predicate \(f : A \times A \to A\) if for all \(a, b, c \in A\) such that \(a\ R\ b\) we have:

Quiz. Function & Predicate congruence [003d]

December 2, 2025

Consider the universe:

\[ U = \{a, b, c\} \]

and the interpretation:

\[ I(=) \triangleq \{\langle a, a \rangle , \langle a, b \rangle , \langle b, a \rangle , \langle b, b \rangle , \langle c, c \rangle \} \]

Does the interpetation \(I(=)\) satisfy the axioms of equality?
Which interpretations for a function \(f\) satisfy the axioms of congruence?
1. \(I(f) \triangleq \{b \to a, a \to c, c \to c\}\)
2. \(I(f) \triangleq \{b \to b, a \to b, c \to b\}\)
3. \(I(f) \triangleq \{b \to a, a \to b, c \to c\}\)

Solution.

December 2, 2025

Yes, the interpretation satisfies the axioms of equality
Going through them one by one:
1. No, because \(f(a) = c\) and \(f(b) = a\) but \(a\ I(=)\ b\) yet \(c\ not\ I(=)\ a\)
2. Yes, because \(f(a) = b\) and \(f(b) = b\) and \(a\ I(=)\ b\) thus \(b\ I(=)\ b\), similarly for \(c\)
3. Yes, because \(f(a) = b\) and \(f(b) = a\) and \(a\ I(=)\ b\) thus \(b\ I(=)\ a\), similarly for \(c\)

Theory of Peano Arithmetic

December 2, 2025

Definition. Theory of Peano Arithmetic [003e]

December 2, 2025

Peano Arithmetic (PA) is a first order theory over the signature \(\Sigma _{PA}\) which contains:

\[ \Sigma _{PA} : \{0, S, +, \times , =\} \]

Where \(0\) is a constant symbol representing zero, \(S\) is a unary function symbol representing the successor function, \(+\) and \(\times \) are binary function symbols representing addition and multiplication respectively, and \(=\) is a binary relation symbol representing equality. The axioms of Peano Arithmetic are:

Quiz. Theory of Peano Arithmetic [003f]

December 2, 2025

Are the following well-formed \(T_{\text {PA}} formulae?\)

\(x + y = 1 \land f(x) = 1 + 1\)
\(\forall x.\ \exists y.\ \exists z.\ x + y = 1\land z \times x = 1 + 1\)
\(2x = y\)

Solution.

December 2, 2025

No, the theory of Peano Arithmetic does not include function symbols like \(f\), nor does it include numerals like \(1\) or \(2\). All terms must be constructed using the constant symbol \(0\), the successor function \(S\), and the function symbols \(+\) and \(\times \).
Yes, this is a well-formed formula. It uses only the symbols and constructs allowed in the theory of Peano Arithmetic.
No, this is not a well-formed formula. The expression \(2x\) is not a valid term in Peano Arithmetic, as numerals like \(2\) are not part of the language. Terms must be built using \(0\), \(S\), \(+\), and \(\times \). A valid way to express the same idea would be \(S(S(0)) \times x = y\). Or if we replace \(S\) with \(1\) then we could do \((1 + 1) \times x = y\)

Theory of Rationals & Integers

December 2, 2025

Definition. Theory of Rationals \(T_{\mathbb {Q}}\) [003i]

December 2, 2025

The theory of rationals \(T_{\mathbb {Q}}\) is a first-order theory over the signature \(\Sigma _{\mathbb {Q}}\) which contains:

\[ \Sigma _{\mathbb {Q}} : \{0, 1, +, -, =, \geq \} \]

(Axioms ommitted for brevity.)

Some important properties of \(T_{\mathbb {Q}}\) are:

Full theory is decidable but doubly exponential.
Conjunctive quantifier-free fragment is efficiently decidable (polynomial time).
\(T_{\mathbb {Q}}\) is the basis for arithemtic reasoning in SMT solvers such as Z3.
In practice the simplex algorithm is used.

Definition. Theory of Presburger Arithmetic [003h]

December 2, 2025

Presburger Arithmetic (PA) is a first order theory over the signature \(\Sigma _{\mathbb {N}}\) which contains:

\[ \Sigma _{\mathbb {N}} : \{0, 1, +, =\} \]

Where \(0\) and \(1\) are constant symbols representing zero and one respectively, \(+\) is a binary function symbol representing addition, and \(=\) is a binary relation symbol representing equality. The axioms of Presburger Arithmetic are:

Some important properties of \(T_{\mathbb {N}} are\):

Validity in quantifer-free Presburger Arithmetic is decidable.
Validity in full Presburger Arithmetic is decidable.
Validity in Presburger Arithmetic has a super exponential complexity \(O(2^{2^n})\)
\(T_{\mathbb {N}}\) is complete, i.e. \[ \forall F.\ T_{\mathbb {N}} \models F \lor T_{\mathbb {N}} \models \neg F \]

Quiz. Theory of rationals \(T_{\mathbb {Q}}\) [003k]

December 2, 2025

Consider the following formula:

\[ \exists x.\ (1 + 1) x = 1 + 1 + 1 \]

Is this formula valid in \(T_{\mathbb {Q}}\)
Is this formula valid in \(T_{\mathbb {Z}}\)

Solution.

December 2, 2025

Yes, this formula is valid in \(T_{\mathbb {Q}}\). In the theory of rationals, we can find a rational number \(x = \frac {3}{2}\) that satisfies the equation \((1 + 1) x = 1 + 1 + 1\). Therefore, there exists an \(x\) in the rationals that makes the equation true.
No, this formula is not valid in \(T_{\mathbb {Z}}\). In the theory of integers, there is no integer \(x\) that satisfies the equation \((1 + 1) x = 1 + 1 + 1\), since \(\frac {3}{2}\) is not an integer. Thus, there does not exist an integer \(x\) that makes the equation true.

Theory of Data structures

December 2, 2025

Definition. Theory of Arrays [003l]

December 2, 2025

The theory of arrays is a first-order theory that models arrays as functions from indices to values. Its signature includes:

\[ \Sigma _A \triangleq \{- [ - ], \langle - \triangleleft - \rangle , =\} \]

where:

\(-[ - ]\): read operation, which takes an array and an index and returns the value at that index.
\(\langle - \triangleleft - \rangle \): write operation, which takes an array, an index, and a value, and returns a new array with the value at the specified index updated.
\(=\): equality relation, which checks if two arrays are identical.

The axioms of the theory of arrays are:

Quiz. Theory of arrays \(T_A\) [003m]

December 2, 2025

Which of the following formula is valid/satisfiable/unsatisfiable ?

\(a[3] = 2\)
\(a \langle 3 \triangleleft 5 \rangle [3] = 5\)
\(a \langle 3 \triangleleft 5 \rangle [3] = 3\)
\(a[3] = 2\land a \langle 3 \triangleleft 5 \rangle [3] = 5\)

Solution.

December 2, 2025

This formula is satisfiable. For example, if we have an array \(a\) such that \(a[3] = 2\), then the formula holds true.
This formula is valid. According to the Read-Over-Write axiom, when we write a value to an index in an array and then read from that same index, we get the value we just wrote. So regardless of the initial contents of array \(a\), after performing the write operation \(a \langle 3 \triangleleft 5 \rangle \), reading from index \(3\) will always yield \(5\) hence making it always true (valid).
This formula is unsatisfiable. According to the Read-Over-Write axiom, when we write a value to an index in an array and then read from that same index, we get the value we just wrote. Therefore, after performing the write operation \(a \langle 3 \triangleleft 5 \rangle \), reading from index \(3\) will always yield \(5\), making it impossible for it to equal \(3\).
This formula is satisfiable. For example, if we have an array \(a\) such that \(a[3] = 2\), then after performing the write operation \(a \langle 3 \triangleleft 5 \rangle \), reading from index \(3\) will yield \(5\). Thus, both parts of the conjunction can be true simultaneously though are not valid in all interpretations.