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 Answer

1

=================

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

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

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

? ; z:=z+y−1 ; z≥y? ~;~ z := z + y – 1 ~;~ z \ge y

You know that ϕ\phi is z≥yz\ge y, you know vv is zz, and you know that ee is z+y−1z + y – 1. So you want to find

ϕ[e/v]=(z≥y)[z+y−1/z]=z+y−1≥y\phi[e/v] = (z \ge y)[z + y – 1 / z] = z + y – 1 \ge y

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

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

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

In part (d), you somehow managed to invoke variables yy and xx 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=−ji = -j. Then you apply i:=i+1i := i + 1, so you can infer i−1=−ji – 1 = -j. Then you apply j=j−1j = j – 1. So you can infer (i−1)=−(j+1)(i – 1) = -(j + 1). And this is only assuming you are dealing with a data structure where +1+1 and −1-1 are inverses. You actually can’t solve this problem otherwise.

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

[B∧P ; S ; Q],[¬B∧P ; T ; Q]P ; if B then S else T endif ; Q\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 BB is z=0z=0, SS is x=z+1x=z+1, QQ is x=1x=1, and TT is x=z−2x=z-2, and PP is unknown. Filling in the blanks, that is:

[z=0∧P ; x=z+1 ; x=1],[¬z=0∧P ; x=z−2 ; x=1]P ; if z=0 then x=z+1 else x=z−2 endif ; x=1\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 PP that satsifies both [z=0∧P ; x=z+1 ; x=1][ z=0 \land P ~;~ x=z+1 ~;~ x=1] and [¬z=0∧P ; x=z−2 ; x=1][\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=⊤P=\top. The second is satisfied by P=((x=1)[z−2/x])P = ((x = 1)[z – 2 / x]) or ¬(¬z=0∧P)\lnot (\lnot z=0 \land P) which is P=0P = 0. So your answer here is correct.

in (d) I meant (| j = |i| |) as postcondition. Is that right? Can you give me more tips for c?

– snnlaynnkrdsm

yesterday

@snnlaynnkrdsm For (c) and (d), just evaluate them from start to finish. For example, after a := 2, you can infer a=2a=2. Then after b := a + 1, you can infer a=2∧b=3a = 2 \land b = 3. For (d), do the same. After i := i + 1, you can infer j=|i−1|j = |i – 1| (assuming +1 and -1 are inverses).

– DanielV

yesterday