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

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

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.

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

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

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

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

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

• x >= 15
• x >= 7
• x >= 11