Hoare triple: Are those hoare triples are correct?

198 Views Asked by At

Below there are some hoare triples. In the questions, either preconditions or postconditions are missed. I completed them under partial correctness. Are they correct?

a. (| ?? |) z=z+y-1; (| z >= y |)
   Answer: (| z > 0 |) z=z+y-1; (| z >= y |)

b. (| ?? |) x=x+1; (| x=y |)
   Answer: (| y = x + 1 |) x=x+1; (| x=y |)

c. (| a=9 |) a=2; b=a+1; a=b*b; (| ?? |)
   Answer: (| a=9 |) a=2; b=a+1; a=b*b; (| a > b |)

d. (| i=-j |) i=i+1; j=j-1; (| ?? |)
   Answer: (| i=-j |) i=i+1; j=j-1; (| y = |x| |)

e. (| ?? |) if (z==0) {x=z+1;} else {x=z-2;} (| x=1 |)
  Answer: (| z = 0 || z = 3 |) if (z==0) {x=z+1;} else {x=z-2;} (| x=1 |)
1

There are 1 best solutions below

7
On

The rule that (a) through (d) is presumably trying to invoke is:

$$\phi[e/v] ~;~ v := e ~;~ \phi$$

(where $A[B/C]$ means all occurences of $C$ are replaced by $B$ in $A$). So for part (a), you have:

$$? ~;~ z := z + y - 1 ~;~ z \ge y$$

You know that $\phi$ is $z\ge y$, you know $v$ is $z$, and you know that $e$ is $z + y - 1$. So you want to find

$$\phi[e/v] = (z \ge y)[z + y - 1 / z] = z + y - 1 \ge y$$

which is the same as $z > 0$, if you assume that we are dealing with integers, but maybe you aren't.

(b) should naturally be $x + 1 = y$, no reason to reverse it.

For (c), $a > b$ isn't your strongest postcondition. You should have $b = 3$, $a = 9$. Just work through the computation directly. This only works if you assume integers.

In part (d), you somehow managed to invoke variables $y$ and $x$ despite them not being part of the probem. This one might be easier to just work forwards again (like in (c)) rather than try to apply the rules:

First you know $i = -j$. Then you apply $i := i + 1$, so you can infer $i - 1 = -j$. Then you apply $j = j - 1$. So you can infer $(i - 1) = -(j + 1)$. And this is only assuming you are dealing with a data structure where $+1$ and $-1$ are inverses. You actually can't solve this problem otherwise.

For part (e), you want to invoke the rule:

$$\frac{[ B \land P ~;~ S ~;~ Q], [\lnot B \land P ~;~ T ~;~ Q]}{P ~;~ \text{if }B \text{ then }S\text{ else }T \text{ endif }~;~Q}$$

So $B$ is $z=0$, $S$ is $x=z+1$, $Q$ is $x=1$, and $T$ is $x=z-2$, and $P$ is unknown. Filling in the blanks, that is:

$$\frac {[ z=0 \land P ~;~ x=z+1 ~;~ x=1], [\lnot z=0 \land P ~;~ x=z-2 ~;~ x=1]} {P ~;~ \text{if }z=0 \text{ then }x=z+1\text{ else }x = z-2 \text{ endif }~;~x=1} $$

So what is the weakest $P$ that satsifies both $[ z=0 \land P ~;~ x=z+1 ~;~ x=1]$ and $[\lnot z=0 \land P ~;~ x=z-2 ~;~ x=1]$? Use the same technique that was used in (a) through (d).

!> The first condition is satisfied by $P=\top$. The second is satisfied by $P = ((x = 1)[z - 2 / x])$ or $\lnot (\lnot z=0 \land P)$ which is $P = 0$. So your answer here is correct.