Lab works: Hoare logic

The following tips can help with proofing correctness.

• After statement x := N, { x = N } holds. We formally prove it as: { N = N } x := N { x = N }.
• Proof rule for assignments is { P[x ↦ e] } x := e { P }. Using bottom-down derivation (forward fashion) all x's in precondition are expressed with e, and then e's are replaced with x resulting in postcondition.
• Because loop invariant must hold in the postcondition of its loop, local variables and loop condition are not part of it.
• When loop invariant is "going through" the loop it can consists local variables. All of these variables should be eliminated before loop terminates.
• It can happen that chosen loop invariant is too week (with it we are unable to deduct the final condition). In this case we can add additional condition D to the invariant. While deriving the postcondition we can independently push D through the loop. This will not mess up our derivation of the proof since; if A ⇒ C hods then, A ∧ B ⇒ C holds too.

Exercise 1

Give a poof of partial and total correctness for the following program with respect to given specifications.

{ x = m ∧ y = n }
x := x + y;
y := x - y;
x := x - y;
{ x = n ∧ y = m }

Exercise 2

Give a poof of partial and total correctness for the following program with respect to given specifications.

{ }
if y < x then
  z := x;
  x := y;
  y := z
else
  skip
end
{ x ≤ y }

Exercise 3

Find a program c, that satisfies the following specification

[ n ≥ 0 ]
c
[ s = 1 + 2 + ... + n ]

and prove its correctness.

Exercise 4

Give a proof of partial and total correctness for the following program with respect to given specifications.

{ x ≥ 0 }
y := 0;
z := x;
while 1 < z - y do
  s := (y + z)/2;
  if s * s < x then
    y := s
  else
    z := s
  end
done
{ y² ≤ x ≤ (y+1)² }