Skip to main content
CSE 331: Software Design & Implementation

CSE 331: Hoare triples practice

Question 1: Hoare Triples

Each row is a Hoare triple about int variables x and y. You may assume no arithmetic here ever overflows.

For each triple, write in its box:

  • T if the triple is valid
  • F if it is not

a.

{{ x = 2 or x = -2 }}
y = x * x;
{{ y = 4 }}
Answer
Valid?
T

Valid: reasoning forward and backward both close.

Forward, from the precondition:

{{ x = 2 or x = -2 }}
y = x * x;
{{ (x = 2 or x = -2) and y = x * x }}
{{ y = 4 }}
  1. The forward rule for y = x * x. Neither the precondition nor x * x mentions y, so nothing is renamed, and the claim gains y = x * x.
  2. Whichever of 2 and -2 x is, x * x is 4. That is the postcondition, so the triple is valid.

Backward, from the postcondition:

{{ x = 2 or x = -2 }}
{{ x * x = 4 }}
y = x * x;
{{ y = 4 }}
  1. Before y = x * x, put x * x for y: the weakest precondition, x * x = 4.
  2. The precondition implies it, whichever of 2 and -2 x is, so the triple is valid.

The rule: Lecture 7's The rules for an assignment.

b.

{{ 0 <= x }}
x = x - 1;
{{ 0 <= x }}
Answer
Valid?
F

Not valid: one state is enough to show it.

A counterexample:

  • Start from x = 0, which the precondition 0 <= x allows.
  • The line makes x equal to -1.
  • Then 0 <= x is false.

The rule: Lecture 7's A triple.

c.

{{ x = y }}
x = x + 1;
{{ x = y + 2 }}
Answer
Valid?
F

Not valid: the postcondition fails in every state the precondition allows.

A counterexample:

  • Start from x = 0 and y = 0, which x = y allows.
  • The line makes x equal to 1.
  • Then x = y + 2 is false: x is 1, and y + 2 is 2.

Backward reasoning shows that every such state fails, not just this one:

{{ x = y }}
{{ x + 1 = y + 2 }}
x = x + 1;
{{ x = y + 2 }}
  1. Before x = x + 1, put x + 1 for x: the weakest precondition, x + 1 = y + 2, that is, x = y + 1.
  2. The precondition, marked, does not imply the claim below it: x = y and x = y + 1 never hold together. The chain breaks here in every state the precondition allows, so the triple is not valid.

The rules: Lecture 7's A triple and The rules for an assignment.

d.

{{ x < y }}
x = x + 1;
{{ x <= y }}
Answer
Valid?
T

Valid, for integers: reasoning forward and backward both close.

Forward, from the precondition:

{{ x < y }}
x = x + 1;
{{ x0 < y and x = x0 + 1 }}
{{ x - 1 < y }}
{{ x <= y }}
  1. The forward rule for x = x + 1. x0 names the old value of x, so the precondition becomes x0 < y, and the claim gains x = x0 + 1.
  2. The old value is x - 1, so put that for x0. Then x = x0 + 1 says nothing, and drops.
  3. For integers, x - 1 < y means x <= y. That is the postcondition, so the triple is valid.

Backward, from the postcondition:

{{ x < y }}
{{ x + 1 <= y }}
x = x + 1;
{{ x <= y }}
  1. Before x = x + 1, put x + 1 for x: the weakest precondition, x + 1 <= y.
  2. For integers, the precondition x < y implies it, so the triple is valid.

Over the real numbers it would not be valid:

  • Start from x = 0 and y = 0.5, which x < y allows.
  • The line makes x equal to 1.
  • Then x <= y is false.

The rule: Lecture 7's The rules for an assignment.

e.

{{ true }}
if (x < 0) {
    x = -x;
}
{{ 0 < x }}
Answer
Valid?
F

Not valid: one state is enough to show it.

A counterexample:

  • Start from x = 0, which the precondition true allows.
  • The condition x < 0 is false, so the branch is skipped, and x stays 0.
  • Then 0 < x is false.

The rule: Lecture 7's A triple.

f.

{{ y = 2 * x }}
y = y + 2;
x = x + 1;
{{ y = 2 * x }}
Answer
Valid?
T

Valid: reasoning forward and backward both close, one line at a time.

Forward, from the precondition, first line first:

{{ y = 2 * x }}
y = y + 2;
{{ y0 = 2 * x and y = y0 + 2 }}
{{ y = 2 * x + 2 }}
x = x + 1;
{{ y = 2 * x0 + 2 and x = x0 + 1 }}
{{ y = 2 * (x - 1) + 2 }}
{{ y = 2 * x }}
  1. The forward rule for y = y + 2. y0 names the old value of y, so the precondition becomes y0 = 2 * x, and the claim gains y = y0 + 2.
  2. The old value is y - 2, so put that for y0: y - 2 = 2 * x, that is, y = 2 * x + 2.
  3. The forward rule for x = x + 1. x0 names the old value of x, and the claim gains x = x0 + 1.
  4. The old value is x - 1, so put that for x0.
  5. 2 * (x - 1) + 2 is 2 * x. That is the postcondition, so the triple is valid.

Backward, from the postcondition, last line first:

{{ y = 2 * x }}
{{ y + 2 = 2 * x + 2 }}
y = y + 2;
{{ y = 2 * x + 2 }}
{{ y = 2 * (x + 1) }}
x = x + 1;
{{ y = 2 * x }}
  1. Before x = x + 1, put x + 1 for x: y = 2 * (x + 1).
  2. Multiplied out, the same claim: y = 2 * x + 2.
  3. Before y = y + 2, put y + 2 for y: the weakest precondition, y + 2 = 2 * x + 2.
  4. The precondition y = 2 * x implies it: add 2 to both sides. So the triple is valid.

The rules: Lecture 7's The rules for an assignment and The rule for a sequence.

g.

{{ 0 < x and 0 < y }}
x = x - y;
{{ 0 < x }}
Answer
Valid?
F

Not valid: the postcondition fails whenever x <= y.

A counterexample:

  • Start from x = 1 and y = 3, which the precondition allows.
  • The line makes x equal to -2.
  • Then 0 < x is false.

Backward reasoning shows exactly which states fail:

{{ 0 < x and 0 < y }}
{{ 0 < x - y }}
x = x - y;
{{ 0 < x }}
  1. Before x = x - y, put x - y for x: the weakest precondition, 0 < x - y, that is, y < x.
  2. The precondition, marked, does not imply the claim below it: from x = 1 and y = 3, it holds and y < x does not. The chain breaks in just the states with 0 < x and x <= y, so the triple is not valid.

The rules: Lecture 7's A triple and The rules for an assignment.

h.

{{ x < y and y < x }}
x = y;
{{ x = y + 1 }}
Answer
Valid?
T

Valid, vacuously: no state makes the precondition true.

Why vacuously:

  • No state has x < y and y < x at once, so the precondition is false.
  • A valid triple asks something only of runs from states where its precondition holds.
  • There are none, so it asks nothing. Lecture 7's {{ false }} x = 0; {{ x = 1 }} is the same case.

Forward, from the precondition:

{{ x < y and y < x }}
{{ false }}
x = y;
{{ false and x = y }}
{{ x = y + 1 }}
  1. No state has x < y and y < x at once, so the precondition is false.
  2. The forward rule for x = y keeps false, and the claim gains x = y.
  3. false implies any claim, the postcondition included, so the triple is valid, vacuously.

Backward, from the postcondition:

{{ x < y and y < x }}
{{ false }}
{{ y = y + 1 }}
x = y;
{{ x = y + 1 }}
  1. Before x = y, put y for x: the weakest precondition, y = y + 1, which no state satisfies.
  2. false implies it, as it implies any claim.
  3. The precondition is false, since no state has x < y and y < x at once. So the triple is valid, vacuously.

The rules: Lecture 7's A triple and The rules for an assignment.

Question 2: Hoare Triples

Each row is a Hoare triple. Variables done and visited have type boolean. All other variables have type int. You may assume no arithmetic here ever overflows.

For each triple, write in its box:

  • T if the triple is valid
  • F if it is not

a.

{{ 0 < y }}
x = x + y;
y = x - y;
{{ y < x }}
Answer
Valid?
T

Valid: the final x exceeds the final y by the original y.

Backward, from the postcondition:

{{ 0 < y }}
{{ (x + y) - y < x + y }}
x = x + y;
{{ x - y < x }}
y = x - y;
{{ y < x }}
  1. Before y = x - y, put x - y for y in the postcondition.
  2. Before x = x + y, put x + y for x in the claim below it.
  3. The claim simplifies to x < x + y, which follows from 0 < y, so the triple is valid.

The rules: Lecture 7's The rules for an assignment and The rule for a sequence.

b.

{{ true }}
if (x == 0) {
    y = 0;
    z = 1;
} else {
    y = 1;
    z = 0;
}
{{ y = 0 and z = 0 }}
Answer
Valid?
F

Not valid: neither branch makes both y = 0 and z = 0 true.

A counterexample:

  • Start from x = 0, y = 0, and z = 0.
  • The condition is true, so the true branch executes.
  • That branch leaves y = 0 and z = 1.
  • The postcondition is false because z = 0 is false.

Why every run fails:

  • The true branch makes y = 0 and z = 1 true.
  • The false branch makes y = 1 and z = 0 true.
  • The conditional rule joins these claims with or, giving (y = 0 and z = 1) or (y = 1 and z = 0).
  • Either way, one of y and z is 1, so y = 0 and z = 0 is false.

The rule: Lecture 7's The rule for a conditional.

c.

{{ done = true or done = false }}
while (!done) {
    done = true;
    visited = true;
}
{{ done = true and visited = true }}
Answer
Valid?
F

Not valid: the body need not execute.

A counterexample:

  • Start from done = true and visited = false, which the precondition allows.
  • The condition !done is false, so the loop ends immediately.
  • visited = true is false in the final state.

The rules: Lecture 7's A triple and Lecture 8's The rule for a while loop.

d.

{{ 0 <= x }}
x = x + 1;
{{ 1 < x }}
Answer
Valid?
F

Not valid: the precondition allows x = 0.

A counterexample:

  • Start from x = 0, which the precondition allows.
  • The assignment makes x = 1.
  • The postcondition requires 1 < x, which is false.

The rule: Lecture 7's The rules for an assignment.

e.

{{ lo <= hi }}
if (x < lo) {
    x = lo;
}
if (hi < x) {
    x = hi;
}
{{ lo <= x and x <= hi }}
Answer
Valid?
T

Valid: the two conditionals make both bounds true.

Forward, from the precondition:

{{ lo <= hi }}
if (x < lo) {
    {{ lo <= hi and x < lo }}
    x = lo;
    {{ lo <= hi and x = lo }}
}
{{ lo <= hi and lo <= x }}
if (hi < x) {
    {{ lo <= hi and lo <= x and hi < x }}
    x = hi;
    {{ lo <= hi and x = hi }}
}
{{ lo <= x and x <= hi }}
  1. The conditional rule adds x < lo in the true branch.
  2. The assignment sets x = lo and preserves lo <= hi.
  3. The conditional rule gives lo <= x from either branch: the true branch sets x = lo, and the empty false branch starts with lo <= x.
  4. The conditional rule adds hi < x in the second true branch.
  5. The assignment sets x = hi and preserves lo <= hi.
  6. The conditional rule gives both bounds from either branch: the true branch has lo <= hi and x = hi, and the empty false branch keeps lo <= x with x <= hi.

The rules: Lecture 7's The rule for a conditional, The rules for an assignment, and The rule for a sequence.

f.

{{ x = y and y = z and x != z }}
x = y;
{{ x != y }}
Answer
Valid?
T

Valid: no state makes the precondition true.

Forward, from the precondition:

{{ x = y and y = z and x != z }}
{{ false }}
x = y;
{{ false and x = y }}
{{ x != y }}
  1. x = y and y = z imply x = z, contradicting x != z.
  2. The forward assignment rule keeps false and adds x = y.
  3. false implies any claim, including x != y, so the triple is valid.

The rules: Lecture 7's A triple and The rules for an assignment.

g.

{{ x = 0 or y = 0 }}
if (x != 0) {
    if (y == 0) {
        x = 1;
        y = 1;
    }
}
{{ x = 0 or y = 0 }}
Answer
Valid?
F

Not valid: the inner true branch can execute.

A counterexample:

  • Start from x = 1 and y = 0.
  • The precondition is true because y = 0.
  • The outer condition x != 0 is true.
  • The inner condition y == 0 is also true.
  • Its assignments leave x = 1 and y = 1.
  • Neither x = 0 nor y = 0 is true in the final state.

The rule: Lecture 7's The rule for a conditional.

h.

{{ 0 <= x }}
while (0 < x) {
    x = x;
}
{{ x = 0 }}
Answer
Valid?
T

Valid: every terminating run from the precondition ends with x = 0.

Forward, with invariant 0 <= x:

{{ 0 <= x }}
{{ Inv: 0 <= x }}
while (0 < x) {
    {{ 0 <= x and 0 < x }}
    x = x;
    {{ 0 <= x }}
}
{{ 0 <= x and x <= 0 }}
{{ x = 0 }}
  1. The precondition is the invariant, so check (1) passes.
  2. The while rule adds the true condition 0 < x at body entry.
  3. x = x leaves x unchanged, preserving the invariant for check (2).
  4. At exit, the while rule gives the invariant and the false condition, x <= 0.
  5. The two bounds force x = 0, so check (3) passes.

When the loop never ends:

  • If x starts positive, the unchanged x keeps the loop running.
  • A valid triple asks only about terminating runs.

The rules: Lecture 7's A triple and Lecture 8's The rule for a while loop.