{x > 10}
if x > 0 then x = -3*x else x = 2*x
{x < 30}
{x < 10}
if x < 0 then x = -3*x else x = 2*x
{x < 30}
{x > 0}
x = x + 10
x = 2*x
{x > 20}
\( \{P\} \; x := max(x, y) \; \{x = y\} \)
Is the following a correct Hoare triple?
\( \{(x \leq 0) \wedge (y \geq 0)\} \; x := max(x, y) \; \{x = y\} \)
True.
Execution of command \(c\) in a state in which \(P\) holds takes the system to a state in which \(Q\) holds. Likewise, Execution of command \(c\) in a state in which \(P'\) holds takes the system to a state in which \(Q\) holds. Therefore execution of \(c\) in a state in which \(P\) or \(P'\) hold takes the system to a state in which \(Q\) holds.
False.
\( [P \Rightarrow True] \)
Substituting True for \(P'\), the right-hand side of the implication becomes \(\{True\} \; c \; \{Q\}\) which states that \(\{Q\}\) holds when \(c\) terminates regardless of the state of when \(c\) is initiated. This is obviously false. For example check that
\( \{x = 1\} \; x = 2*x \; \{x = 0\} \)
is False.
True
If \(c\) is executed in a state in which \(P'\) holds then --- because \([P' \Rightarrow P]\) --- \(P\) also holds in that state and so \(Q\) holds when \(c\) terminates.
{x > 10}
if x > 0 then x = -3*x else x = 2*x
{x < 30}
True.
Because the precondition \(x > 10\) implies the if-clause (\(x > 0\)), the above Hoare triple holds if the following triple holds
{x > 10}
x = -3*x
{x < 30}
We can check that this triple holds by substituting the right-hand
side of the assignment statement to \(x\) for \(x\) in the
postcondition: So we replace \(x < 30\) by:
\( -3*x < 30 \)
Which is equivalent to \(x < 10\), which is satisfied by the precondition.
{x < 10}
if x < 0 then x = -3*x else x = 2*x
{x < 30}
False.
When \(x = - 11\), the precondition is satisfied. The if-clause \(x < 0\) holds. So the assignment statement \(x = -3 *x\) is executed which makes \(x = 33\) which violates the postcondition.
{x > 0}
x = x + 10
x = 2*x
{x > 20}
True
Again we can verify this by working backwards from the postcondition. Substitute the right-hand side of the assignment to \(x\) for \(x\) in the postcondition; i.e. substitute \( 2*x\) for \(x\) in \( x > 20\) to get \(2*x > 20\). This is equivalent to \(x > 10\).
Now do the same step for the previous statement: \(x + 10 > 10\). This is equivalent to \(x > 0\) which is satisfied by the precondition.
We can annotate the program with assertions to make it clearer.
{x > 0}
x = x + 10
{x > 10}
x = 2*x
{x > 20}
\( \{P\} \; x := max(x, y) \; \{x = y\} \)
Answer
Substitute the right-hand side, i.e., \(max(x, y)\), of the assignment for the left-hand side, i.e., \(x\), in the postcondition, i.e., \(x = y\) to get:\( max(x, y) = y \) which simplifies to:
\( x \leq y \)
The answer is \(P \equiv (x \leq y)\), and we have the following Hoare triple:
\( \{x \leq y\} \; x := max(x, y) \; \{x = y\} \)
Question
Is the following a correct Hoare triple?\( \{(x \leq 0) \wedge (y \geq 0)\} \; x := max(x, y) \; \{x = y\} \)
Answer
Yes because \((x \leq 0) \wedge (y \geq 0)\) is stronger than the precondition \(x \leq y\), i.e.,\( [((x \leq 0) \wedge (y \geq 0)) \quad \Rightarrow \quad (x \leq y)] \)
K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology