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