CSE 331: Loop checks practice

Question 1: Loop Invariants

Here is a loop, with the claim that holds just before it and the postcondition after it. Every variable here is an int. You may assume no arithmetic here ever overflows.

{{ 0 <= n and i = 0 and s = 0 }}
{{ Inv: I }}
while (i < n) {
    i = i + 1;
    s = s + 2;
}
{{ s = 2 * n }}

Recall the three checks of the rule for a while loop, with P the claim before the loop, b its condition, and Q the postcondition:

Check (1): P implies I.
Check (2): {{ I and b }} body {{ I }} is valid.
Check (3): I and not b implies Q.

For each candidate I, write in each check's box:

Y if the check passes
N if it fails

	Check (1)	Check (2)	Check (3)
A. `{{ s = 2 * i }}`
B. `{{ 0 <= i and i <= n and s = 2 * i }}`
C. `{{ i <= n and s = 2 * i }}`
D. `{{ 0 <= i and i <= n }}`
E. `{{ s = 2 * i + 2 }}`
F. `{{ i < n and s = 2 * i }}`

A. {{ s = 2 * i }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	N

It holds each time the loop tests its condition, but it is too weak at the exit: it says nothing about how i compares with n.

Check (1) passes.

The check: P implies I.
P gives i = 0 and s = 0.
Then s = 2 * i reads 0 = 2 * 0, which is true.

Check (2) passes.

The check: {{ I and b }} body {{ I }} is valid: a pass that begins with I and b ends with I.
A pass begins with s = 2 * i.
The body adds 2 to s.
It also adds 1 to i, and so 2 to 2 * i.
Both sides grow by 2, so s = 2 * i holds again.

Check (3) fails.

The check: I and not b implies Q.
I says nothing about how i compares with n.
A counterexample: n = 0, i = 1, s = 2.
- I is true: 2 = 2 * 1.
- not b is true: 1 < 0 is false.
- Q fails: s is 2, not 2 * 0.
- No run reaches this state, but the check asks about every state where I and not b is true.

The rule: Lecture 8's The rule for a while loop.

B. {{ 0 <= i and i <= n and s = 2 * i }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	Y

It proves the loop correct: all three checks pass.

Check (1) passes.

The check: P implies I.
P gives i = 0, 0 <= n, and s = 0.
So 0 <= i, i <= n, and s = 2 * i all hold.

Check (2) passes.

The check: {{ I and b }} body {{ I }} is valid: a pass that begins with I and b ends with I.
A pass begins with 0 <= i, i <= n, s = 2 * i, and i < n.
The body adds 1 to i, which stays at least 0, and is now at most n, since it was less than n.
So 2 * i grows by 2, and the body adds 2 to s as well.
Both sides grow by 2, so s = 2 * i holds again.

Check (3) passes.

The check: I and not b implies Q.
i <= n and not i < n give i = n.
Then s = 2 * i = 2 * n, which is Q.

The rule: Lecture 8's The rule for a while loop.

C. {{ i <= n and s = 2 * i }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	Y

It proves the loop correct too: no check needs B's 0 <= i.

Check (1) passes.

The check: P implies I.
P gives i = 0, 0 <= n, and s = 0.
So i <= n and s = 2 * i hold.

Check (2) passes.

The check: {{ I and b }} body {{ I }} is valid: a pass that begins with I and b ends with I.
A pass begins with i <= n, s = 2 * i, and i < n.
The body adds 1 to i, which is now at most n, since it was less than n.
So 2 * i grows by 2, and the body adds 2 to s as well.
Both sides grow by 2, so s = 2 * i holds again.
Nothing here needs 0 <= i, which B has and C does not.

Check (3) passes.

The check: I and not b implies Q.
i <= n and not i < n give i = n.
Then s = 2 * i = 2 * n, which is Q.

The rule: Lecture 8's The rule for a while loop.

D. {{ 0 <= i and i <= n }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	N

It holds each time the loop tests its condition, but it says nothing about s, so it cannot give Q.

Check (1) passes.

The check: P implies I.
P gives i = 0 and 0 <= n.
So 0 <= i and i <= n hold.

Check (2) passes.

The check: {{ I and b }} body {{ I }} is valid: a pass that begins with I and b ends with I.
A pass begins with 0 <= i, i <= n, and i < n.
The body adds 1 to i, which stays at least 0, and is now at most n, since it was less than n.

Check (3) fails.

The check: I and not b implies Q.
I says nothing about s.
A counterexample: n = 0, i = 0, s = 1.
- I is true: 0 <= 0 and 0 <= 0.
- not b is true: 0 < 0 is false.
- Q fails: s is 1, not 2 * 0.
- No run reaches this state, but the check asks about every state where I and not b is true.

The rule: Lecture 8's The rule for a while loop.

E. {{ s = 2 * i + 2 }}

Answer

Check (1)	Check (2)	Check (3)
N	Y	N

The body keeps it true, but P makes it false at the start, and at the exit it does not give Q.

Check (1) fails.

The check: P implies I.
P gives i = 0 and s = 0.
I needs s = 2 * 0 + 2, which is 2.
A counterexample: n = 0, i = 0, s = 0.
- P is true.
- I fails: s is 0, not 2.

Check (2) passes.

The check: {{ I and b }} body {{ I }} is valid: a pass that begins with I and b ends with I.
A pass begins with s = 2 * i + 2.
The body adds 2 to s.
It also adds 1 to i, and so 2 to 2 * i + 2.
Both sides grow by 2, so s = 2 * i + 2 holds again.

Check (3) fails.

The check: I and not b implies Q.
The false condition gives n <= i.
At exit, I gives s = 2 * i + 2, at least two more than Q asks.
A counterexample: n = 0, i = 0, s = 2.
- I is true: 2 = 2 * 0 + 2.
- not b is true: 0 < 0 is false.
- Q fails: s is 2, not 2 * 0.
- No run reaches this state, but the check asks about every state where I and not b is true.

The rule: Lecture 8's The rule for a while loop.

F. {{ i < n and s = 2 * i }}

Answer

Check (1)	Check (2)	Check (3)
N	N	Y

It can be false at the start, and the last pass breaks it; check (3) passes only because I and not b is never true.

Check (1) fails.

The check: P implies I.
P allows n = 0, and then i < n is false.
A counterexample: n = 0, i = 0, s = 0.
- P is true.
- I fails: 0 < 0 is false.

Check (2) fails.

The check: {{ I and b }} body {{ I }} is valid: a pass that begins with I and b ends with I.
The last pass makes i equal to n, and then i < n is false.
A counterexample: n = 1, i = 0, s = 0.
- I and b is true: 0 < 1 and 0 = 2 * 0.
- The body makes i equal to 1 and s equal to 2.
- I fails: 1 < 1 is false.

Check (3) passes.

The check: I and not b implies Q.
I and not b has both i < n and not i < n, which never hold together.
So I and not b is false, and false implies anything: the check passes, vacuously.

The rule: Lecture 8's The rule for a while loop.

Question 2: Loop Checks: Find the First Negative

Arrays are non-null. n is the length of a and does not change. a[l..r] is the slice starting at l and ending just before r. An empty slice has length 0. Array equality compares the elements. Every numeric variable and array element is an int. You may assume no arithmetic here ever overflows. An empty slice contains no negative values and contains only positive values.

{{ i = 0 }}
{{ Inv: I }}
while (i < n && 0 <= a[i]) {
    i = i + 1;
}
{{ 0 <= i <= n and a[0..i] contains no negative values
   and (i = n or a[i] < 0) }}

Recall the three checks, with P the claim just before the loop, c its condition, and Q its postcondition:

Check (1): P implies I.
Check (2): {{ I and c }} body {{ I }} is valid.
Check (3): I and not c implies Q.

Check each separately, including states that initialization never reaches. The stated array shapes and unmodified inputs apply in every check; the initial values in P are available only in check (1).

For each candidate I, write in each check's box:

Y if the check passes
N if it fails

	Check (1)	Check (2)	Check (3)
A. `{{ 0 <= i <= n and a[0..i] contains no negative values }}`
B. `{{ 0 <= i <= n }}`
C. `{{ 0 <= i <= n and a[0..i] contains only positive values }}`
D. `{{ 0 <= i <= n and (i = 0 or 0 <= a[0]) }}`
E. `{{ 0 <= i < n and a[0..i] contains no negative values }}`
F. `{{ i = 0 }}`

A. {{ 0 <= i <= n and a[0..i] contains no negative values }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	Y

Check (1) passes.

The initial prefix is empty, so it contains no negative values.

Check (2) passes.

The condition says the next element is nonnegative.
Extending the prefix by that element preserves the claim and keeps i <= n.

Check (3) passes.

With i in range, the false condition means either i = n or a[i] < 0.
The candidate rules out any earlier negative value.

The rule: Lecture 8's The rule for a while loop.

B. {{ 0 <= i <= n }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	N

Check (1) passes.

i = 0 is within the bounds for every array length.

Check (2) passes.

The condition gives i < n, so adding 1 keeps the index within the bounds.

Check (3) fails.

The candidate says nothing about earlier elements.
A negative value before i would mean that i is not the first negative position.
A counterexample:
- Before: n = 1; a = [-1]; i = 1.
- The candidate is true.
- The condition is false.
- The postcondition is false.

The rule: Lecture 8's The rule for a while loop.

C. {{ 0 <= i <= n and a[0..i] contains only positive values }}

Answer

Check (1)	Check (2)	Check (3)
Y	N	Y

Check (1) passes.

The initial empty slice contains no value that violates positivity.

Check (2) fails.

The condition allows a zero, but appending zero breaks strict positivity.
A counterexample:
- Before: n = 1; a = [0]; i = 0.
- The candidate is true before the body.
- The condition is true before the body.
- After: n = 1; a = [0]; i = 1.
- The candidate is now false.

Check (3) passes.

Positive values are nonnegative.
Thus there is no earlier negative value.
The false condition supplies the same exit cases as in A.

The rule: Lecture 8's The rule for a while loop.

D. {{ 0 <= i <= n and (i = 0 or 0 <= a[0]) }}

Answer

Check (1)	Check (2)	Check (3)
Y	Y	N

Check (1) passes.

Initially i = 0, so the first alternative holds.
The initial index is in range.

Check (2) passes.

If i = 0, the loop condition requires 0 <= a[0].
If 0 < i, the candidate already requires 0 <= a[0].
The array does not change.
The condition i < n keeps the new index in range.

Check (3) fails.

The first element can be nonnegative even though a later processed element is negative.
A counterexample:
- Before: n = 2; a = [0, -1]; i = 2.
- The candidate is true.
- The condition is false.
- The postcondition fails.

The rule: Lecture 8's The rule for a while loop.

E. {{ 0 <= i < n and a[0..i] contains no negative values }}

Answer

Check (1)	Check (2)	Check (3)
N	N	Y

Check (1) fails.

The empty array is allowed, and its initial index satisfies i = n, not i < n.
A counterexample:
- Before: n = 0; a = []; i = 0.
- The precondition is true.
- The candidate is false.

Check (2) fails.

Processing a nonnegative final array element makes i = n, breaking the strict bound.
A counterexample:
- Before: n = 1; a = [0]; i = 0.
- The candidate is true before the body.
- The condition is true before the body.
- After: n = 1; a = [0]; i = 1.
- The candidate is now false.

Check (3) passes.

The strict bound rules out exiting because the index reached n.
The false condition therefore gives a[i] < 0.
The prefix claim rules out earlier negative values.

The rule: Lecture 8's The rule for a while loop.

F. {{ i = 0 }}

Answer

Check (1)	Check (2)	Check (3)
Y	N	Y

Check (1) passes.

The precondition sets i = 0.

Check (2) fails.

Every body execution changes i to 1.
A counterexample:
- Before: n = 1; a = [0]; i = 0.
- The candidate is true before the body.
- The condition is true before the body.
- After: n = 1; a = [0]; i = 1.
- The candidate is now false.

Check (3) passes.

With i = 0, the false condition means the array is empty or its first element is negative.
In either case the prefix is empty and the postcondition holds.

The rule: Lecture 8's The rule for a while loop.