Tute (Week 9)
Table of Contents
1 David Gries‘ coffee beans
A bag of coffee beans contains beans which are either black or white. Take any two beans from the bag at random: if they have different colours, throw away the white bean, but put the black bean back into the bag. If on the other hand they have the same colour, throw away both beans; but then add (back) a new white bean into the bag (from our infinite supply of extra white beans on the side). Repeat this process until there’s only one bean left.
- Suppose you know how many beans there are of each colour initially. From that, can you predict the colour of the last bean?
- Write down a program in the language \(\mathcal{L}^+\) that models this process by updating two variables \(b\) (number of black beans) and \(w\) (number of white beans). Use the non-deterministic choice operator \(+\) to model the act of picking two beans at random.
- What is the variant of the program you wrote just above?
- Write a loop invariant that can be used to verify that your prediction (from the first question) is correct.
- The parity of the number of black beans is an invariant. Hence, if we had an even number of black beans initially, the final bean will be white; if we had an odd number, it will be black.
This uses the encoding of \(\mathbf{while}\) presented in the lectures. That is, \(\mathbf{while}\ b\ \mathbf{do}\ P\ \mathbf{od}\) should be understood as shorthand for \((b; P)^*; \neg b\).
\begin{array}{l} \mathbf{while}\ (b + w > 1)\ \mathbf{do} \\ \quad (b > 1; b := b -2; w := w + 1) \\ \quad +\ (b > 0 \wedge w > 0; w := w - 1) \\ \quad +\ (w > 1; w := w - 1) \\ \mathbf{od} \end{array}Each loop iteration is a non-deterministic choice between drawing two black beans, two different beans, or two white beans. Each choice is guarded by a check that makes sure we have enough beans to actually make this draw.
- The variant is \(b + w\).
An invariant is: \[b \mathop{\mathsf{mod}} 2 = N \wedge b \ge 0 \wedge w \ge 0\] where \(N\) is an integer constant that doesn't depend on any of the program variables.
You can also mention the specific parity, which means you'd technically need two separate Hoare logic proofs for the even and odd cases, respectively. \[odd(b) \wedge b \ge 0 \wedge w \ge 0\]
2 Extending our Language
Suppose we wanted to extend \(\mathcal{L}\) with a "repeat" loop
\[ \mathbf{do}\ s\ \mathbf{until}\ b\]
that runs the loop body \(s\) at least once: it checks the guard of the loop only after each iteration of the loop body, exiting the loop if the guard is true.
- Propose a translation of this repeat loop into existing \(\mathcal{L}\) constructs.
Validate your translation by showing that the following Hoare logic rule for the repeat loop is derivable for your translation:
\[ \dfrac{ \{ \varphi \}\ s\ \{ \varphi \} }{\{ \varphi \}\ \mathbf{do}\ s\ \mathbf{until}\ b\ \{ \varphi \land b \} }\quad. \]
- \(s; \mathbf{while}(\neg b)\ \mathbf{do}\ s\ \mathbf{od}\)
- This proof tree elides the rule names, as well as a couple of implications of the form \(A \rightarrow A\) from the rule of consequence: \[\dfrac{ \{ \varphi \}\ s\ \{ \varphi \} \quad \dfrac{ \dfrac{ \dfrac{\varphi \wedge \neg b \rightarrow \varphi \quad \{ \varphi \}\ s\ \{ \varphi \} } {\{ \varphi \wedge \neg b \}\ s\ \{ \varphi\}} } { \{ \varphi \}\ \mathbf{while}(\neg b)\ \mathbf{do}\ s\ \mathbf{od}\ \{ \varphi \land \neg \neg b \} } \quad \varphi \land \neg\neg b \rightarrow \varphi \land b } { \{ \varphi \}\ \mathbf{while}(\neg b)\ \mathbf{do}\ s\ \mathbf{od}\ \{ \varphi \land b \} } } { \{ \varphi \}\ s; \mathbf{while}(\neg b)\ \mathbf{do}\ s\ \mathbf{od}\ \{ \varphi \land b \} } \]
3 Program algebra
Program algebra is the manipulation of program texts in a way that preserves their meaning, and (hopefully) leads to a better or more understandable program than before. An example is the equality between these two programs:
\[[\![ x := 1; y := 2 ]\!] = [\![ y := 2; x := 1 ]\!]\]
For these two programs, at least sequential composition commutes. But it is not the case, in general, that,
\[[\![ P; Q ]\!] = [\![ Q; P ]\!]\]
- Find a counterexample to the above formula; or, in other words, show that sequential composition is not commutative.
- Show that sequential composition is associative.
What is the identity element of sequential composition? Or in other words, what is a program \(P\) such that for all \(Q\),
\[[\![ P; Q ]\!] = [\![ Q; P]\!] = [\![ Q]\!]\]
- Are the following algebraic laws true in general or not? \[[\![ \mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od} ]\!] = [\![ P; \mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od} ]\!]\] \[[\![ \mathbf{if}\ g\ \mathbf{then}\ P;Q\ \mathbf{else}\ P;R\ \mathbf{fi} ]\!] = [\![ P; \mathbf{if}\ g\ \mathbf{then}\ Q\ \mathbf{else}\ R\ \mathbf{fi} ]\!]\] \[[\![ \mathbf{while}\ g\ \mathbf{do}\ (\mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od})\ \mathbf{od} ]\!] = [\![ \mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od} ]\!]\] \[[\![ \mathbf{while}\ g\ \mathbf{do}\ (\mathbf{while}\ g'\ \mathbf{do}\ P\ \mathbf{od})\ \mathbf{od} ]\!] = [\![ \mathbf{while}\ g \wedge g'\ \mathbf{do}\ P\ \mathbf{od} ]\!]\]
- For example, let \(P = x := 1\) and \(Q = x := 2\). The final value of \(x\) will be different depending on which one happens last.
Step by step, as follows:
\begin{array}{lcll} [\![ (P; Q); R ]\!] & = & [\![ P; Q]\!]; [\![ R ]\!] & (definition) \\ & = & ([\![P]\!]; [\![Q]\!]); [\![ R ]\!] & (definition) \\ & = & [\![P]\!]; ([\![Q]\!]; [\![ R ]\!]) & (assoc.\ of\ relational\ composition) \\ & = & [\![P]\!]; [\![Q; R ]\!] & (definition) \\ & = & [\![P; (Q; R)]\!] & (definition) \end{array}- The identiy element of sequential composition is \(\mathbf{skip}\). The semantics of \(\mathbf{skip}\) is the identity relation, so the identity laws follow from the fact that the identity relation is the left and right identity of relational composition.
- As follows:
- It is not the case that \[[\![ \mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od} ]\!] = [\![ P; \mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od} ]\!]\] because the two exhibit different behaviour if \(g\) is false initially.
- It does not hold that \[[\![ \mathbf{if}\ g\ \mathbf{then}\ P;Q\ \mathbf{else}\ P;R\ \mathbf{fi} ]\!] = [\![ P; \mathbf{if}\ g\ \mathbf{then}\ Q\ \mathbf{else}\ R\ \mathbf{fi} ]\!]\] because executing \(P\) may change the truth value of \(g\). If \(P\) cannot change the truth value of \(g\), it becomes provable.
- It does hold that \[[\![ \mathbf{while}\ g\ \mathbf{do}\ (\mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od})\ \mathbf{od} ]\!] = [\![ \mathbf{while}\ g\ \mathbf{do}\ P\ \mathbf{od} ]\!]\] Two key facts about the relational operators (not proved here) are used in its proof: \[(R^*)^* = R^*\] \[(\langle g \rangle; (\langle g \rangle; R)^*)^* = (\langle g \rangle; R)^* \]
- It is not the case that \[[\![ \mathbf{while}\ g\ \mathbf{do}\ (\mathbf{while}\ g'\ \mathbf{do}\ P\ \mathbf{od})\ \mathbf{od} ]\!] = [\![ \mathbf{while}\ g \wedge g'\ \mathbf{do}\ P\ \mathbf{od} ]\!]\] Consider the case where \(g = \top\) and \(g' = \bot\). The former will loop forever, but the latter will not.