1. Yes, \(p\) is an atom.
2. Yes, \(p\) is a literal. Literals are either atoms or negated atoms, and since \(p\) is an atom, it is also a literal.
3. Yes, \(p\) is a formula. Formulas can be literals, and since \(p\) is a literal, it is also a formula.
4. \(\neg p\) is not an atom, but it is a literal (as it is a negated atom) and therefore also a formula.
5. \(\neg \neg p\) is a formula, since the inner negation \(\neg p\) is a literal and any additional negation applied promotes it to a formula. In other words only negated atoms are literals but negated literals are formulas. This is especially important when we later discuss Negation Normal Form (NNF).

So we can see that the interpretation does not satisfy the formula. In other words for this assignment the formula does not hold true. Given that this is a somewhat simple formula we could also just see this by observation, i.e.

For the second formula lets just go with the simpler approach again, so we have

So in this case the formula is satisfied by the interpretation.

• A formula is satisfiable if there exists at least one combination of true/false assignments to its variables that makes the formula true.
• A formula is unsatisfiable if there is no combination of true/false assignments to its variables that makes the formula true (i.e., it is always false).
• A formula is valid (or a tautology) if it is true under all possible combinations of true/false assignments to its variables.

Now we can analyze each formula:

1. For the lhs to be true both p and q must be true. However, if p is true then \(\neg p\) is false, making the implication false. If p is false then the implication is vacuously true regardless of what we set q to. Thus, this formula is satisfiable (e.g., when p is false) but not valid (e.g., when p and q are true).
2. If both p and q are true then the lhs is true and so is the rhs by virtue of p being true. If p is false then the implication is vacuously true regardless of q. If q is false then the rhs is true regardless of p. Thus, this formula is valid as it is true for all combinations of truth values for p and q.
3. The first part \((p \to (q \to r))\) is true unless p is true and either q or r is false. The second part \(\neg ((p \land q) \to r)\) is true when p and q are true but r is false. Thus we can satisfy the entire formula by setting p and q to true and r to false. However, if we set p to false then the first part is vacuously true, but the second part becomes false. Thus, this formula is falsifiable (e.g., when p and q are true and r is false) but not valid (e.g., when p is false).

1. True. Both sides are always false.
2. True. Both sides are always true.
3. False. Left side is always false, right side is always true.
4. True. This is De Morgan's law. Good to remember \[ \neg (p \land q) \equiv \neg p \lor \neg q \]
5. False. Left side is true when p is true, right side is true when either p or q is true.
6. True. Double negation elimination.

1. No. The implication operator \(\to \) is not allowed in NNF.
2. Yes. Negations are only applied to literals, and only \(\land \) and \(\lor \) are used.
3. No. The negation operator \(\neg \) is applied to a non-literal formula \((\neg r \land s)\).
4. No. The double negation \(\neg \neg r\) is not allowed in NNF. Important to remember since that can trip you up.

1. \(f(x)\): Invalid, as \(f\) is a function symbol and cannot stand alone as a formula.
2. \(p(x)\): Valid, as \(p\) is a relation symbol applied to the term \(x\).
3. \(p(f(x))\): Valid, as \(f(x)\) is a term and \(p\) is a relation symbol applied to that term.
4. \(p(p(x))\): Invalid, as \(p(x)\) is a formula, not a term, and cannot be an argument to \(p\).
5. \(p(f(f(x)))\): Valid, as \(f(x)\) is a term, and applying \(f\) again yields another term, which can be an argument to \(p\).

1. \(y\) is bound, as it is within the scope of the quantifier \(\forall y\).
2. The first occurrence of \(x\) is bound, as it is within the scope of the quantifier \(\forall x\).
3. The second occurrence of \(x\) is free, as it is not within the scope of any quantifier that binds it.

1. \(\langle I, \sigma \rangle (f(a, y)) = I(f)(\langle I, \sigma \rangle (a), \langle I, \sigma \rangle (y)) = I(f)(I(a), \sigma (y)) = I(f)(1, 1) = 2\)
2. \(\langle I, \sigma \rangle (f(x, b)) = I(f)(\langle I, \sigma \rangle (x), \langle I, \sigma \rangle (b)) = I(f)(\sigma (x), I(b)) = I(f)(2, 2) = 1\)
3. \(\langle I, \sigma \rangle (f(f(x, b), f(a, y))) = I(f)(\langle I, \sigma \rangle (f(x, b)), \langle I, \sigma \rangle (f(a, y))) = I(f)(1, 2) = 2\)

1. \(p(f(b), f(x))\) evaluates to \(\top \) because \(f(b) = f(\beta ) = \alpha \) and \(f(x) = f(\alpha ) = \beta \), and \(p(\alpha , \beta ) = \top \).
2. \(p(f(x), f(b))\) evaluates to \(\top \) because \(f(x) = f(\alpha ) = \beta \) and \(f(b) = f(\beta ) = \alpha \), and \(p(\beta , \alpha ) = \top \).
3. \(p(a, f(x))\) evaluates to \(\bot \) because \(a = \alpha \) and \(f(x) = f(\alpha ) = \beta \), and \(p(\alpha , \beta ) = \bot \).

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

As a reminder we are working with the axiom:

1. 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.
2. 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\).
3. 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.

1. 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\).
2. No, a formula can be valid in all \(T\)-models, but false in some non-\(T\)-model. Hence its not necessarily valid in FOL.

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

1. Yes, the interpretation satisfies the axioms of equality
2. 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\)

1. 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 \).
2. Yes, this is a well-formed formula. It uses only the symbols and constructs allowed in the theory of Peano Arithmetic.
3. 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\)

1. 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.
2. 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.

1. This formula is satisfiable. For example, if we have an array \(a\) such that \(a[3] = 2\), then the formula holds true.
2. 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).
3. 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\).
4. 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.

1. Starting in the state \(x \mapsto 2\) we evaluate \(x := x - 1\) to the state \(x \mapsto 1\)
2. 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*} \]
3. 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*} \]
4. 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.
5. 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 '\).

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

1. 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\).
2. 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\).
3. 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\).
4. 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\).
5. 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.

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

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

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

but let's now assume the following initial state:

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:

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

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:

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

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

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:

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:

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.

1. 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.
2. 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) \]
3. 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) \]
4. Yes, this is just correct by definition of a substitution leaving irrelevant variables unaffected.

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:

So if we have that:

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:

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

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.

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.

1. Yes, this is provable, removing a conjunct is a common way of weakening an expresison as we are removing one condition.
2. Yes, this is provable, same reasoning as in (1)
3. 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\)
4. 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.
5. 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

1. 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.
2. 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.
3. No, this is quite easy to see as it immediately fails even before we get into the loop as \(0 \geq 10 \to \bot \).

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

1. 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
2. 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.
3. 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.

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:

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:

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

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

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:

By the sequence and precondition strengthening rule we have that

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

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.

we can think of this as defining the function:

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

1. If \(i = 1\) then we have \[ a'[i] = a[1] = 2 \to a'[i] = 3 \equiv 2 = 3 \equiv \bot \]
2. 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:

Now testing this rule on the first hoare triple:

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

substituting in our \(R\) we get

after a reduction we have

simplifying this we get

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

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:

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

1. This formula is satisfiable. For example, if we have an array \(a\) such that \(a[3] = 2\), then the formula holds true.
2. 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).
3. 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\).
4. 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.

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

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

1. 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\).
2. \(\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:

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

As a reminder, a Hoare triple:

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

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:

The idea of backwards reasoning here is as follows:

1. 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:
2. 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.
3. 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.
4. 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}\).

1. We again start from our post-condition then proceed with a case split or more accurately an inversion on the evaluation rule.
2. 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:

1. Seeing how a term must have been derived
2. 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:

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

1. 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} \]
2. 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) \]
3. 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.
4. Same reasoning as above, but now it works since \[ y > -1 \to y + 1 > 0 \] indeed makes sense

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.

We introduce a new construct \(\texttt {fail}\) which denotes the failure state, as an alternative to \(\sigma \).

For the assumption we only have a \(\top \) rule, the idea being if the assumption holds then the statement is equivalent to a \(\texttt {skip}\) otherwise the execution gets stuck but doesn't fail.

The idea with getting stuck being that since we aren't failing for the case of partial-correctness (failure or termination) it means we can simply ignore this case.

The final big-step evaluation rule is for the havoc statement:

In addition to our big-step evaluation rules we also have Hoare rules.

A central thing to understand with assertions especially is that they integrate a result's monad into the big-step evaluation semantics, in addition to the Hoare logic. So the idea is now instead of the relationship being denoted by:

It's now expressed as

Where we can model \(\texttt {Result}\) as the following monad

    inductive Result (α : Type)
    | ok : α → Result α      -- Normal termination with final state
    | fail : Result α        -- Assertion failure / error state
    deriving Repr, DecidableEq
  

At this point if you want to be pedantic it's worth mentioning that the implication is that we are lifting all other inference rules into the context of this result monad, though for pedagogical purposes its enough to just assume that \(\Downarrow \sigma \) just corresponds to \(\Downarrow \texttt {.ok} \sigma \) i.e. evaluated into a non-fail state.

The Hoare triple is where stuff becomes a bit more interesting. As a reminder, the classical hoare triple is basically just an alias for the logical formula:

Naturally because we know are no longer evaluating into just \(\sigma '\) but either an \(\texttt {ok}\) or \(\texttt {fail}\) state, it's worth asking how we actually represent that as a Hoare triple. We can start in much the same way as we do for the regular partial correctness hoare triple

Here we then run into I guess a design choice as to how we proceed, the two main possibilities are:

• We fail sometimes succeed other times this would mean that: \[ (\exists \sigma ', \sigma _t = \texttt {.ok}\ \sigma ' \land Q(\sigma ')) \] another way of seeing this is here we are disallowig failure meaning that for a hoare triple to be proven valid we must explicitly demonstrate as a side condition that we cannot fail otherwise our hoare triple is invalid.
• We never fail which would mean that: \[ (\forall \sigma ', \sigma _t = \texttt {.ok}\ \sigma ' \land Q(\sigma ')) \] for this rule another way of seeing it is we are ignoring failure or filter success states since we are clearly only quantifying over those states that are successfull.

The latter option seems to be generally more common in theoretical settings because it doesn't require explicitly accounting for failure states, they are just implicitly filtered out in the logic.

We can remember that the weakest precondition is simply what we can derive reasoning backwards from the formulaic expression of a hoare triple.

1. Considering our wp formula we have \[ \texttt {wp}(\texttt {assert}(b), Q)(\sigma ) \to (\texttt {assert}(b), \sigma ) \Downarrow \texttt {.ok}\ \sigma \to Q(\sigma ) \] reasoning backwards we can start with a case split on the evaluation of the assertion, this leads to two cases
   • \(b\) evaluates to true, as this case trivially implies that the assertion evaluates into \(\texttt {.ok}\ \sigma \) it means we must prove \(Q(\sigma )\). The only way we can prove this is by having our weakest precondition be a witness to this assertion.
   • \(b\) evaluates to false, as this would imply a contradiction since the assertion evaluates to \(\texttt {.ok}\ \sigma \), more specifically we know have to prove the contradiction that \(\texttt {.ok}\ \sigma = \texttt {.fail} \sigma \), we know (i.e. have a hypothesis) by inversion that \(b \Downarrow ^f \sigma \) since we know \(b\) has to be true to prove the contradiction we also must ensure the weakest precondition states that \(b \Downarrow ^t \sigma \)
   from these two cases we can conclude that two demonstrate the soundness of the weakest precondition for assert statements, it must be the case that the \(\texttt {wp}\) is the conjunction of the postcondition and the logical assertion that what is being asserted is indeed true, so we have that \[ \texttt {wp}(\texttt {assert}(b), Q)(\sigma ) \equiv (b \Downarrow ^t \sigma ) \land Q(\sigma ) \] the more intuitive reasoning here is that \(Q\) should hold before and after as an assert should, just by design, not do anything to the memory, it's only an assertion after all. Additionally, the condition should hold true as \(\texttt {wp}\) definitionally describes a set of states where all terminating executions end in a state satisfying \(Q\) thus if \(b\) does not evaluate to true, there is no terminating execution from \(\sigma \).
2. We can just use the more intuitive reasoning here, we know the weakest precondition characterizes a set of states where terminating executions end in a state satisfying \(Q\). The only way for something being assumed to be true leading to some other else is it if implies something else, thus our \(\texttt {wp}\) becomes \[ \texttt {wp}(\texttt {assume}(b), Q)(\sigma ) \equiv (b \Downarrow ^t \sigma ) \to Q(\sigma ) \] in terms of backward reasoning the idea is that \(\texttt {assume}(p)\) essentially just adds a raw hypothesis \((b \Downarrow ^t \sigma )\) but clearly that by itself doesn't somehow allow me to just manifest \(Q(\sigma )\), the only way we could possibly get \(Q\) from \(b\) being true is if we have a function which states that \(b\) being true implies \(Q\).

1. No, we can draw the dependency graph as follows

2. Yes, because the head \(p\) depends on the query \(r\) and vv. again as a graph we can draw it as follows

Let's consider a basic instance of abstraction where we think of the concrete domain as set's of numbers and the abstract domain as rangers or intervals of numbers which characterize these sets. So formally we say

• Our concrete domain is the power set \(\mathcal P(\mathbb {R})\) of the natural real numbers \(\mathbb {R}\) ordered by set-inclusion so \(\sqsubseteq \equiv \subseteq \)
• Our abstract domain is represented by intervals in addition to the symbols for true and false, so \[ A = \textrm {Intervals} \cup \{\top , \bot \} \]
• Our concretization function maps from an interval to all those numbers contained within the interval, so as an example \[ \gamma ([l, u]) \equiv \{x \mid l \leq x \leq u\} \]
• Our abstraction function which takes a concrete element \(c\) then maps this to the meet or conjunct of all abstract element in which the ordering with the concretization function holds, i.e. \[ \alpha (c) = \bigwedge \{a \in A \mid c \subseteq \gamma (a)\} \] the idea is that it represents the most precise abstract representation which can capture the concrete element c. Operationally we can express this equivalently as \[ \alpha(c \equiv \{x_1, x_2, \ldots, x_n\}) = \begin{cases} [\textrm{min}\ c, \textrm{max}\ c] & \textrm{if bounded} \\ [\textrm{min}\ c, +\infty) & \textrm{if only lb} \\ (-\infty, \textrm{max}\ c] & \textrm{if only ub} \\ \top & \textrm{if unbounded} \\ \bot & \textrm{if}\ = \emptyset \end{cases} \] so more plainly we can understand the abstraction function of just being the most exact combination i.e. meet / conjunction of intervals to express our concrete element.

A common application within the domain of logic and computer science is to consider the concrete domain as referring to formulas or equivalently set's of states, not too much unlike our power-set of numbers. With our abstract state then being a conjunct of predicates from some finite set \(P\) which best characterize our concrete formulas.

• Each element in the abstract domain is some permutation of our finite predicate set \(P\), so we have \[ A = \mathcal P(P) \quad P_1 \sqsubseteq P_2 \iff P_2 \subseteq P_1 \] each abstract element \(a \in P\) is defined by the conjunction \[ \bigwedge _{p \in a} p \] hence our concretization function yields those set's of concrete states (or predicates representing these states) which satisfy \(a\). \[ \gamma (a) = \{\sigma \in \Sigma \mid \forall p \in a.\ p(\sigma ) = \top \} \equiv \llbracket \bigwedge _{p \in a} p \rrbracket \]
• The abstraction function is then defined more or less the usual way, we take in a concrete set of states \(c\) then aggregate those predicates which describe our concrete set of states most precisely. \[ \alpha (c) = \bigcap \{a \in A \mid c \subseteq \gamma (a)\} \] can equivalent formulation is \[ \alpha (c) = \bigwedge \{p \in P \mid c \to p\} \]

Let's consider as an example

Here we can define the abstraction function as follows

Our usual strongest postcondition can be understood as a mapping from a concrete domain to a concrete domain, i.e.

Where \(C\) represents our concrete domain, in the world of program logic this is typically assertions on the state of some memory environment. The idea behind the abstract \(\texttt {sp}\), is that we have a function

In other words we are considering the strongest postcondition from within the abstract domain. Intuitively this just means that our predicates or assertions on the memory states (or equivalently the set of states we characterize) will be expressed in abstract terms.

The abstract strongest postcondition, denoted \(\texttt {sp}^\#\) or \(\textrm {post\#}\) is defined as

Let's explain a bit on how we can derive this, we begin with the idea that for each \(a \in A\) and each statement \(s\) we want:

This expresses soundness in other words, the resulting set of states, generated by concretizing the abstraction \(a\) must be contained within the prediction of the abstract transformer predicate \(\texttt {sp}^\#\). Then using the Galois connection we have between \(\alpha \) and \(\gamma \)

which expresses the notion that \(c\) is approximated by \(a\). We can rewrite our earlier soundness condition as:

two again denote the same conceptual thing that our abstract predicate transformer \(\texttt {sp}^\#\) is an over-approximation of the analogous transformer for the concrete domain. As we would preferably like to have the most precise approximation we choose equality. Or stated differently by definition the most precise abstracted approximation of the strongest post-condition we can have for some abstracted state is literally just this state concretized, and the resulting set abstracted.

The most important property to remember about the abstract strongest post-condition is that if we do over-approximate an error state it does not allow us to conclude that the program is wrong.

Content

Definition text...

Definition text...

Definition text...

Content

Content

Example content...

Content

Example content...