Hoare Logic and Proving a Program Meets Its Specification · seed 1 · A4, ink-friendly. The answer key prints on its own page for grown-ups.

Proving code correct with Hoare triples

Computing · Software Engineering · ages 23-24
Name ______________________   Date ____________

  1. Which fact must be checked when a loop is entered?

    • The proposed invariant holds after the initialization
    • The proposed invariant forces the guard to remain true
    • The proposed invariant was discovered without any tool

  2. What does the partial-correctness triple {P} C {Q} promise?

    • Code C terminates from every starting state, even when P is false
    • Code C terminates from P, even when its final state does not satisfy Q
    • If code C starts in P and terminates, its final state satisfies Q

  3. The valid triples {x = 0} x := x + 1 {x = 1} and {x = 2} y := x {y = 2} can be composed directly using those intermediate assertions.

    Circle one:   True   False

  4. Let m >= 1 be a fixed integer. Run j := 1; while j < m do j := j + 1. Invariant j >= 1 is preserved but cannot prove j = m at exit. Which repair should be checked?

    • Keep j >= 1 and add j >= m before every iteration begins
    • Weaken to j >= 0 and keep no upper bound on j throughout
    • Try 1 <= j <= m; recheck entry, preservation and exit

  5. Over mathematical integers, start with x = 4 and run x := x + 3; y := 2*x. Which intermediate and final facts justify the composition?

    • After the first line x = 7; after the second y = 8
    • After the first line x = 7; after the second y = 14
    • After the first line x = 4; after the second y = 14

  6. A verification-condition generator sends a formula to a solver, which returns unknown. What follows?

    • The obligation remains unproved; correctness is not established
    • The obligation is false; the program must have a reachable failure
    • The obligation is valid; the solver has completed the required proof

  7. The loop while true do skip preserves invariant true. Does that establish termination?

    • It terminates because its invariant always remains true
    • It terminates because an empty step cannot change any state
    • No; this loop repeats forever while preserving its invariant

  8. Over mathematical integers, what is the weakest precondition of x := x + 4 for postcondition x >= 11?

    • x >= 15
    • x >= 7
    • x >= 11
LightMySky · lightmysky.comW1-mt_bJZnbBrUIP-s1

Answer key

For grown-ups. Fold this page away before handing over the rest.

Proving code correct with Hoare triples W1-mt_bJZnbBrUIP-s1

  1. The proposed invariant holds after the initialization · The invariant must hold before the first iteration. Its source, whether a person or a tool, does not replace this check.
  2. If code C starts in P and terminates, its final state satisfies Q · Partial correctness guarantees the postcondition if execution starts in a state satisfying the precondition and terminates. It does not prove termination.
  3. False · The first postcondition x = 1 does not imply the second precondition x = 2. Those assertions do not justify composition.
  4. Try 1 <= j <= m; recheck entry, preservation and exit · The upper bound j <= m holds initially and survives increment under j < m. At exit, j >= m combines with it to give j = m.
  5. After the first line x = 7; after the second y = 14 · The first line gives x = 4 + 3 = 7. The second uses that updated value, giving y = 2 x 7 = 14.
  6. The obligation remains unproved; correctness is not established · Unknown supplies neither a proof of validity nor a refutation. The obligation remains open.
  7. No; this loop repeats forever while preserving its invariant · The guard stays true and skip leaves the state unchanged. The loop repeats despite preserving its invariant.
  8. x >= 7 · Substitute x + 4 for x in the postcondition: x + 4 >= 11. This is equivalent to x >= 7.
Worksheet · LightMySky