SE 504   Spring 2026
HW #5: Pencil-and-paper Program Correctness Proofs
Due: 5:00pm, Thursday, April 9

Recall the following:

Relationship between Hoare Triples and the weakest precondition function:

wp Assignment Law: [wp.(x:=E).Q  ≡  Q(x:=E)], from which we derive

Hoare Triple Assignment Law: {{P}} x:=E {{Q}}  ≡  [P ⇒ Q(x:=E)].

wp Sequential Composition Law: [wp.(S₁; S₂).Q  ≡  wp.S₁.(wp.S₂.Q)], from which we derive

Hoare Triple Sequential Composition Rule: To prove the Hoare Triple {P} S₁; S₂ {Q}, it suffices to devise a predicate R and to prove both {P} S₁ {R} and {R} S₂ {Q}. If S₂ is an assignment command (or any other sequence of commands for which wp.S₂.Q is easily found), the obvious choice for R is wp.S₂.Q.

1. Prove the correctness of this program:

{{x = X ∧ y = Y}} x := x + y; y := x - y; x := x - y {{x = Y ∧ y = X}}

The wp Conditional Command Law says that if IF is the program if B then S else T fi , then

From that we derive the Hoare Triple Conditional Command Law, which says that

2. Prove the validity of this Hoare Triple: {{P ∧ 0≤k<b.Length}} if b[k] ≤ 0 then sum,k := sum - b[k], k+1; else sum := sum + b[k]; k := k+1; fi {{P ∧ 0≤k≤b.Length}}

3. Prove the validity of this Hoare Triple: {{P ∧ 0≤k<b.Length}} if b[k] ≤ 0 then sum := sum - b[k]; else sum := sum + b[k]; fi k := k+1; {{P ∧ 0≤k≤b.Length}}

where P: sum = (+i | 0 ≤ i < k : |b[i]|).

The absolute value function satisfies this condition:

Notice that, in Problem 2, the two branches of the selection command are different in that one is a simultaneous assignment and the other is a sequential composition of two assignments. Hence their proofs should not be mirror images of one another.

Notice that, in Problem 3, the program itself is a sequential composition of a selection command and an assignment command. This is unlike Problem 2, whose program is a selection command. Hence the two proofs, while having some commonality, should not be the same.

In each of the remaining problems, you are given a Hoare triple of the form {{P}} S_init; while B { S } {{Q}} (possibly with some missing pieces) in which S_init is an assignment command (used for initialization), B is a loop guard, and S is a loop body. The Hoare triple is annotated with a loop invariant I and bound function t.

Prove it by showing each of the five proof obligations for a loop:

1. {{P}} S_init {{I}}, which guarantees that the initialization truthifies the loop invariant (just before the loop's first iteration).
2. {{I ∧ B}} S {{I}} which guarantees that each iteration of the loop preserves the truth of the loop invariant.
3. [I ∧ ¬B  ⟹  Q], which guarantees that, if the loop terminates, the postcondition will hold at that time.
4. [I ∧ B  ⟹  t > 0] which guarantees that, as long as more iterations of the loop are to occur, the bound function has not yet descended to the threshold of zero.
5. {{I ∧ B ∧ t=C}} S {{t < C}} which guarantees that each iteration of the loop causes the value of the bound function to decrease.

Items (i) and (ii) together show that I is, as claimed, an invariant of the loop. Item (iii) shows that, if and when the loop terminates, the postcondition Q holds. Items (iv) and (v) together show that the loop terminates after finitely many iterations.

Note that any precondition regarding only constants (e.g., N≥0) can be considered as an implicit part of the loop invariant.

4. Prove the correctness of this program (the input to which is the array b[]).

k, sum := 0,0; {{ loop invariant I: sum = (+i | 0≤i<k : |b[i]|) ∧ 0≤k≤b.Length }} {{ bound function t: b.Length - k }} while k ≠ b.Length { if b[k] ≤ 0 then sum := sum - b[k]; else sum := sum + b[k]; fi k := k+1; } {{ Q: sum = (+i | 0≤i<b.Length : |b[i]|) }}

Do not repeat the work that you did for Problem 3, but include a remark that justifies the claim that the answer to Problem 3 suffices as a proof of (ii).

• empty denotes the empty list;
• head.z denotes the first element of the (necessarily non-empty) list z;
• tail.z denotes the list obtained by removing the head of the (necessarily non-empty) list z.
• ⊕ denotes the "insert element at beginning of list" operator (commonly known as the cons constructor).
• The vertical bar, |, denotes list concatenation (also known as append), which has higher precedence than = but lower than both function application and the ⊕ operator.

You may make use of the following axioms and theorems:

For all b:Elem and  z,z1,z2 : list of Elem, Axiom 1: empty | z  =  z     (empty is left identity of  | ) Axiom 2: z | empty  =  z     (empty is right identity of  | ) Axiom 3: (b ⊕ z1) | z2  =  b ⊕ (z1 | z2)     (mutual associativity of ⊕, | ) Theorem 1: (b ⊕ empty) | z  =  b ⊕ z     (from Axioms 1,3) Theorem 2: (z1 | z2) | z3  =  z1 | (z2 | z3)     (associativity of  | ) Axiom 4: (z != empty) ≡ (z = head.z ⊕ tail.z)     (defn of head, tail) Axiom 5a: rev.empty = empty     (defn of rev) Axiom 5b: rev.(b ⊕ z)  =  rev.z | (b ⊕ empty)     (defn of rev) Theorem 3: rev.z1  |  b ⊕ z2  =  rev.(b⊕z1) | z2     (useful property of rev) Axiom 6a: length.empty = 0     (defn of length) Axiom 6b: length.(b⊕z)  =  1 + length.z     (defn of length) Theorem 4: length.z ≥ 0     (lower bound of length)

Here is the program (the input to which is the list Z).

var x, y : list of Elem; x,y := Z, empty; {{invariant I: Z = rev.y | x}} {{bound t: length.x}} while x ≠ empty { x,y := tail.x, head.x ⊕ y; } {{Z = rev.y}}