CSE 331�Software Design & Implementation
Summer 2026
Section 4 – Loop Invariants & ADTs
Specifications for ADTs – Review
public class List {
final int hd;
final List tl;
}
State Representations
Internally Documenting ADTs – Review
Abstract Function (AF) – defines what abstract state the field values represent
Representation Invariants (RI) – facts about the field values that must always be true
Documenting ADTs – Example
// A list of integers that can retrieve the last element in O(1)
interface FastList {
/**
* Returns the object as a regular list
* @returns this
*/
List toList();
}
class FastLastList implements FastList {
// RI: this.last = last(this.list);
// AF: this = this.list;
// @returns last(this)
int getLast() {
return this.last;
};
}
Hide the representation details (i.e. real fields) from the client
Talk about functions in terms of the abstract state (this)
Externally Documenting ADTs - Review
* @modifies states what could be mutated by function (this)
* @effects Detailed description of guaranteed changes
/**
* High level description of what function does
* @param a What "a" represents + any conditions
* @requires Rules about multiple params and Abstract State (this)
* @returns Detailed description of return value
* @throws Condition when errors will be thrown
*/
Loop Invariant – Review
true!
{{Inv: I}}
while (cond) {
S
}
true!
true!
true!
Question ….
Where is it allowed for a loop invariant not to hold?
Question ….
Where is it allowed for a loop invariant not to hold?
Task 1 - Everybody Loops
Goal:
Show that our loop correctly computes the quotient of x / 10.
I.e., that the loop correctly finds the largest integer y such that 10y ≤ x.
10(y+1) is TOO LARGE.
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task a)
Fill in P1. Then, show that the invariant is true when we get to the top of the loop for the first time.
i.e., show that P1 implies the loop invariant
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task a)
Fill in P1. Then, show that the invariant is true when we get to the top of the loop for the first time.
i.e., show that P1 implies the loop invariant
How does P1 imply the loop invariant?
Goal: Show both parts of the invariant using facts from P1.
Since:
x = x_0 and y = 0
We can subtract 10y from the right side, giving the first fact from the invariant:
x_0 - 10y = x
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task a)
Fill in P1. Then, show that the invariant is true when we get to the top of the loop for the first time.
i.e., show that P1 implies the loop invariant
How does P1 imply the loop invariant?
Goal: Show both parts of the invariant using facts from P1.
Since:
x_0 >= 0 and x = x_0
We can substitute in for x_0, giving the second fact from the invariant:
x >= 0
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task a)
Fill in P1. Then, show that the invariant is true when we get to the top of the loop for the first time.
i.e., show that P1 implies the loop invariant
How does P1 imply the loop invariant?
Goal: Show both parts of the invariant using facts from P1.
Since:
x_0 >= 0 and x = x_0
We can substitute x for x_0, giving the second fact from the invariant:
x >= 0
Task 1 - Everybody Loops (Math ver.)
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
The first part of the invariant holds
x_0 - 10y = x - 10y since x = x_0
= x since y = 0
Task 1 - Everybody Loops (Math ver.)
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
The first part of the invariant holds
x_0 - 10y = x - 10y since x = x_0
= x since y = 0
The second fact holds since x = x_0 >= 0
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task b)
Fill in P2. Then, show that Q1 holds when we exit the loop
i.e., show that P1 implies the loop invariant
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
How does P2 imply Q1?
Goal: Show all parts of Q1 using our facts from P2
From the invariant in P2, we know:
x_0 - 10y = x and x >= 0
Substituting x >= 0 into x_0 - 10y = x and adding 10y to both sides gives the first fact in Q1:
10y <= x_0.
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
How does P2 imply Q1?
Goal: Show all parts of Q1 using our facts from P2
From P2, we know:
x_0 - 10y = x and x < 10.
Substituting x < 10 into x_0 - 10y = x and adding 10y to both sides gives x_0 < 10y + 10 which can be rewritten to show the second fact of Q1:
x_0 < 10(y + 1).
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
How does P2 imply Q1?
Goal: Show all parts of Q1 using our facts from P2
The third fact of Q1 is given to us in P2:
x_0 - 10y = x.
Task 1 - Everybody Loops (Math ver.)
b) Fill in P2, then show that Q1 holds when we exit the loop.
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
When we exit the loop, we know that P2: inv (x_0 - 10y = x, x ≥ 0), and x < 10. The first part of the postcondition holds since
10y = x_0 - x since x_0 - 10y = x
Task 1 - Everybody Loops (Math ver.)
b) Fill in P2, then show that Q1 holds when we exit the loop.
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
When we exit the loop, we know that P2: inv (x0 - 10y = x, x ≥ 0), and x < 10. The first part of the postcondition holds since
10y = x_0 - x since x_0 - 10y = x
≤ x_0 since x ≥ 0
Task 1 - Everybody Loops (Math ver.)
b) Fill in P2, then show that Q1 holds when we exit the loop.
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
When we exit the loop, we know that P2: inv (x0 - 10y = x, x ≥ 0), and x < 10. The first part of the postcondition holds since
10y = x_0 - x since x_0 - 10y = x
≤ x_0 since x ≥ 0
the second part of the postcondition holds since
x_0 = x + 10y since x_0 - 10y = x
Task 1 - Everybody Loops (Math ver.)
b) Fill in P2, then show that Q1 holds when we exit the loop.
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
When we exit the loop, we know that P2: inv (x0 - 10y = x, x ≥ 0), and x < 10. The first part of the postcondition holds since
10y = x_0 - x since x_0 - 10y = x
≤ x_0 since x ≥ 0
the second part of the postcondition holds since
x_0 = x + 10y since x_0 - 10y = x
< 10 + 10y since x < 10
Task 1 - Everybody Loops (Math ver.)
b) Fill in P2, then show that Q1 holds when we exit the loop.
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
When we exit the loop, we know that P2: inv (x0 - 10y = x, x ≥ 0), and x < 10. The first part of the postcondition holds since
10y = x_0 - x since x_0 - 10y = x
≤ x_0 since x ≥ 0
the second part of the postcondition holds since
x_0 = x + 10y since x_0 - 10y = x
< 10 + 10y since x < 10
= 10(y + 1)
Task 1 - Everybody Loops (Math ver.)
b) Fill in P2, then show that Q1 holds when we exit the loop.
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
And the third part is a restatement of the first fact from the invariant. Because the method returns y, and Q implies the required bounds for the quotient, the code correctly satisfies the @return specification.
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task c)
Fill in Q2. Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.
Hint: What do we know at the end of a loop?
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task c)
Fill in Q2. Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task c)
Fill in Q2. Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
Task c)
Fill in Q2. Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
How does P3 imply Q2?
Goal: Show all parts of Q2 using our facts from P3
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
How does P3 imply Q2?
Goal: Show all parts of Q2 using our facts from P3
From P3, we know:
x_0 - 10(y - 1) = x + 10.
Multiplying through and subtracting 10 from both sides gives the first part of the invariant from Q2.
x_0 - 10y = x
Task 1 - Everybody Loops
// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
{{ x = x_0 and x_0 >= 0 }}
int y = 0;
{{ P1: x = x_0 and x_0 >= 0 and y = 0 }}
{{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}
{{ P2: Inv (x_0 - 10y = x and x >= 0) and x < 10 }}
{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
return y;
}
How does P3 imply Q2?
Goal: Show all parts of Q2 using our facts from P3
From P3, we know:
x + 10 >= 10
Subtracting 10 from both sides gives the second part of the invariant from Q2.
x >= 0
Task 1 - Everybody Loops (Math ver.)
c) Fill in Q2 (Hint: what do we know at the end of a loop?). Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.
{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
We must show P3 implies the invariant:
From P3, we know that x0 - 10(y - 1) = x + 10. Simplifying this:
x0 - 10y + 10 = x + 10
x0 - 10y = x
Also from P3, we know x + 10 >= 10. Subtracting 10 from both sides gives us x >= 0. Thus, the invariant holds.
Array Notation (Review)
Other useful facts:
*The “⧺” symbol represents concatenation between two lists.
Task 2 – Rally the Loops
/**
* Writes over each copy of y in A with the value z.
* @param A the array to replace values in
* @param y the value to be replaced in A
* @param z the value to replace y with in A
* @modifies A
* @effects A = A_0 with every instance of y replaced
* with a z
*/
public void replace(int[] A, int y, int z) { .. }
In this problem, we’ll be implementing the following function:
Task 2 – Rally the Loops
int i = ____________________
// Inv: A[0 .. i] = A_0[0 .. i] with every y replaced with a z
// and A[i .. A.length] = A_0[i .. A.length]
while (________________________________________) {
}
Fill in the missing parts of the code, to make it correct with the given invariant:
Task 2 – Rally the Loops
int i = 0;
// Inv: A[0 .. i] = A_0[0 .. i] with every y replaced with a z
// and A[i .. A.length] = A_0[i .. A.length]
while ( i < A.length ) {
}
Fill in the missing parts of the code, to make it correct with the given invariant:
Task 2 – Rally the Loops
int i = 0;
// Inv: A[0 .. i] = A_0[0 .. i] with every y replaced with a z
// and A[i .. A.length] = A_0[i .. A.length]
while ( i < A.length ) {
if (A[i] == y) {
A[i] = z;
}
i++;
}
Fill in the missing parts of the code, to make it correct with the given invariant:
Task 2 – Rally the Loops
int i = ____________________
// Inv: A[0 .. i] = A_0[0 .. i] and A[i .. A.length] =
// A_0[i .. A.length] with every y replaced with a z
while (________________________________________) {
}
Fill in the missing parts of the code, to make it correct with the given invariant:
Task 2 – Rally the Loops
int i = A.length;
// Inv: A[0 .. i] = A_0[0 .. i] and A[i .. A.length] =
// A_0[i .. A.length] with every y replaced with a z
while ( i > 0 ) {
}
Fill in the missing parts of the code, to make it correct with the given invariant:
Task 2 – Rally the Loops
int i = A.length;
// Inv: A[0 .. i] = A_0[0 .. i] and A[i .. A.length] =
// A_0[i .. A.length] with every y replaced with a z
while ( i > 0 ) {
i--;
if (A[i] == y) {
A[i] = z;
}
}
Fill in the missing parts of the code, to make it correct with the given invariant:
Task 3 - Rich AF
Consider three different concrete representations for MutableIntSet:
public class MutableIntSetImpl implements MutableIntSet {
(1) // AF: this = this.elems[0 .. size]
private int[] elems;
private int size;
(2) // AF: this = this.elems[0 .. size]
// RI: this.elems contains no dups
private int[] elems;
private int size;
(3) // AF: this = this.elems[0 .. size]
// RI: this.elems is sorted
private int[] elems;
private int size;
public MutableIntSetImpl(int[] elems) {
this.elems = elems;
this.size = elems.length;
}
Task 3 - Rich AF
public boolean contains(int n) {
return Arrays.binarySearch(this.elems, n) >= 0;
}
Task 3 - Rich AF
public boolean contains(int n) {
return Arrays.binarySearch(this.elems, n) >= 0;
}
This implementation satisfies the specification only with concrete representation (3). When the array is not sorted, binarySearch is not guaranteed to find the element when present.
Task 3 - Rich AF
b) State the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. Why?
public boolean contains(int n) {
for (int i = 0; i < this.elems.length; i++) {
if (this.elems[i] == n)
return true;
}
return false;
}
Task 3 - Rich AF
b) State the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. Why?
public boolean contains(int n) {
for (int i = 0; i < this.elems.length; i++) {
if (this.elems[i] == n)
return true;
}
return false;
}
This implementation satisfies the specification with any of the concrete representations because it does not require any representation invariant to hold.
Task 3 - Rich AF
c) State the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. Why?
public void add(int n) {
if (!this.contains(n)) {
if (size >= this.elems.length) {
int[] temp = new int[size * 2 + 1];
for (int i = 0; i < this.elems.length; i++) {
temp[i] = this.elems[i];
}
this.elems = temp;
}
this.elems[size++] = n;
}
}
Task 3 - Rich AF
c) State the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. Why?
This satisfies the specification of add with concrete representations (1--2). This holds trivially for (1) since it has no representation invariant, and it holds with (2) because this implementation ensures no duplicates. It would not satisfy the spec with concrete representation (3) because it does not ensure that the array is sorted.
Task 3 - Rich AF
d) State the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. Why?
public boolean remove(int n) {
for (int i = 0; i < this.elems.length; i++) {
if (this.elems[i] == n) {
size--;
for (int j = i; j < size - 1; j++) {
this.elems[j] = this.elems[j + 1];
}
return true;
}
}
return false;
}
Task 3 - Rich AF
d) State the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. Why?
This satisfies the specification with concrete representations (2). It works with (2) because removing an element preserves the fact that there are no duplicates. It also preserves the sorting property required by (3); however, it still does not work with (3) or (1) because removing a single element does not leave an array not containing the element if there was more than one copy in the array.
MutableIntSet ADT
/**
* Represents a **mutable** integer set, or a collection of distinct integers.
*/
public class MutableIntSet {
/**
* Determines whether n is in the set.
* @param n the number to look for in the set
* @return true if n is in the set, false otherwise
*/
public boolean contains(int n);
/**
* Adds n to the set if not already present.
* @param n the number to add to the new set.
* @modifies this
* @effects this is unchanged if this_0 contains n
* otherwise, this contains all of this_0 and n
*/
public void add(int n);
/**
* Removes the desired int from the set.
* @param n The int to remove
* .... To complete in part d
*/
public boolean remove(int n);
}
Task 4 - Good News and Add News
MutableIntSet T = {1, 2, 3}
Task 4 - Good News and Add News
@modifies says that add may or can modify this but it is not a promise that it does so. For example, in this case we know this would not be modified (via its spec) since the set already contains 3.
MutableIntSet T = {1, 2, 3}
Task 4 - Good News and Add News
b) Consider the following static method:
/**
* Adds n to the set if not already present.
* @param old the set to add to
* @param n the number to add to the new set.
* @requires old is not null
* @return a set with n and all of the elements of old.
* If old.contains(n), the new set has all the same elements as 'old'.
*/
public static MutableIntSet add(MutableIntSet old, int n);
Now, consider a call T.add(4). Explain how the operation of MutableIntSet.add differs from that of a call to static add(T, 4) in terms of this.
Task 4 - Good News and Add News
b) Now, consider a call T.add(4). Explain how the operation of MutableIntSet.add differs from that of a call to static add(T, 4) in terms of this.
MutableIntSet.add actually changes the abstract state (this) to contain n, whereas the static (immutable) add method returns a new set and implicitly promises not to modify old by not having an @modifies clause.
Task 4 - Good News and Add News
c) What is the abstract state of 𝑇 after the following code (This is forward reasoning.):
T.add(4);
T.add(2);
T.add(0);
MutableIntSet T = {1, 2, 3}
Task 4 - Good News and Add News
c) What is the abstract state of 𝑇 after the following code (This is forward reasoning.):
T.add(4);
T.add(2);
T.add(0);
The resulting state would be {0, 4, 1, 2, 3}.
MutableIntSet T = {1, 2, 3}
Task 4 - Good News and Add News
d) Write a specification for the method remove. You should have two cases - n is in the set, and n is not. Clearly explain how the abstract state changes after the method call and what is returned.
Task 4 - Good News and Add News
d) One possible solution:
/**
* Removes the desired int from the set. Returns true if
* successful, false if the int isn't in this set.
* @param n The int to remove.
* @modifies this
* @effects if this_0 contains n, this = this_0 with n removed.
* If this_0 does not contain n, this = this_0.
* @returns true if this_0 contains n, false otherwise.
*/
public boolean remove(int n);
Fin
Remember to submit your half-sheets!