CSE 331�Software Design & Implementation

​

Autumn 2026

Section 3 – Reasoning

Warm-Up (Hoare Triple Validity)

For each of the following Hoare Triples, decide whether it is valid or invalid. �If it is invalid, provide a counterexample.

Administrivia

• HW2 is due Friday @ 11:59 pm!
• Reading 3 releases Friday and will be due next Friday @ 11:59pm!

​

​

​

3

Forward Reasoning – Review

• Forward reasoning fills in the postcondition
• Gives strongest postcondition making the triple valid
• Apply forward reasoning to fill in R

​

​

​

​

​

​

​

• Check second triple by proving that R implies Q

R

P

{{P}}

S

{{R}}

{{Q}}

Forward Reasoning Basic Example

{{ w > 0 }}

x = 17;

{{ }}

y = 42;

{{ x - 1 > 1 and y = 3 * x }}

z = w + x + y;

{{ x - 1 > 1 and y = 3 * x and z = y + 1 }}

​

w > 0 and x = 17

w > 0 and x = 17 and y = 42

w > 0 and x = 17 and y = 42 and z = w + x + y

​

Append new facts to your collection as you move down the code

Notice that we did not combine or drop any facts

Forward Reasoning Tools

• Subscripts
• Append new facts with subscripts to represent them
• Gets messy quickly in complex or strange programs
• The extra detail helps us represent everything

​

• Invertible operations
• Use algebra to put the expression in terms of the old value
• Much more readable but not everything can be inverted
• Ex: Integer division dealing with truncation

Forward Reasoning Error Example

{{ x > 1 }}

x = x + 1;

{{ x = x₀ + 1 and x₀ > 1 }}

y = 3 * x;

{{ x = x₀ + 1 and y = 3 * x }}

z = y + 1;

{{ x = x₀ + 1 and z = (3 * x) + 1 }}

​

​

What’s wrong with these assertions?

​

Drops this assertion

Substitutes/simplifies assertions too early by dropping y variable relationship to x

Corrected Forward Reasoning Example

{{ x > 1 }}

x = x + 1;

{{ x₀ > 1 and x = x₀ + 1 }}

y = 3 * x;

{{ x₀ > 1 and x = x₀ + 1 and y = 3 * x }}

z = y + 1

{{ x₀ > 1 and x = x₀ + 1 and y = 3 * x and z = y + 1 }}

does not simplify assertions early or drop variable relationships

Invertible Operation Examples

• The assignment is x = x₀ + 1 so x₀ = x - 1�

{{ x = y }}

x = x + 1;

{{ x - 1 = y }} or equivalently {{ x = y + 1 }}

​

• The rules fall apart here since we truncate the result so we can’t know what the previous value was�

{{ x = 8 }} {{ x = 9 }}

x = x / 2; x = x / 2;

{{ x = 4 }} {{ x = 4 }}

Backward Reasoning

• Backwards reasoning fills in preconditions
• Just use substitution!
• Gives weakest precondition making the triple valid
• Apply backwards reasoning to fill in R

​

​

​

​

​

​

​

• Check first triple by proving that P implies R

​

​

R

Q

{{P}}

{{R}}

S

{{Q}}

Backwards Reasoning Basic Example

{{ [2 - 4(9 + c)] / 7 < 5 }}

a = 9 + c;

{{ (2 - 4a) / 7 < 5 }}

b = 4a;

{{ (2 - b) / 7 < 5 }}

c = 2 - b;

{{ c / 7 < 5 }}

d = c / 7;

{{ d < 5 }}

[2 - 4(9 + c)] / 7 < 5

(2 - 4a) / 7 < 5

(2 - b) / 7 < 5

c / 7 < 5

1. start with the postcondition

(input)

2. backwards substitution

(plug and chug)

3. end at the precondition

(output)

Forward & Backward General Rules

Forward Reasoning Tools:

• Subscripts or invertible operations
• Either tool is fine

​

Backward Reasoning Tools:

• Substitution

​

General:

• Do not drop a fact if it still says something useful
• Understand how to use both forward reasoning tools!

Simplifying Assertions

{{ [2 - 4(9 + c)] / 7 < 5 }} ←→ {{c > -69 / 4}}

a = 9 + c;

{{ (2 - 4a) / 7 < 5 }}

b = 4a;

{{ (2 - b) / 7 < 5 }}

c = 2 - b;

{{ c / 7 < 5 }}

d = c / 7;

{{ d < 5 }}

[2 - 4(9 + c)] / 7 < 5

(2 - 4a) / 7 < 5

(2 - b) / 7 < 5

c / 7 < 5

{{ original assertion }} ←→ {{ simplified assertion }}

Task 1b & Task 2.a

• Task 1.b (forward reasoning)
• Great practice for subscripts and invertible operations.
• Task 2.a (backwards reasoning)

Try these on your own time! Time estimate: ~20 minutes

Task 1 - Found Guilty of Reason

1. Use forward reasoning to fill in the missing assertions in the following code. Use invertible operations.

{{y > 5 and z > 2}}

x = 4 * y - 3

{{-}}

y = y - 5

{{-}}

z = z * y

{{P: }}

{{Q: x < 2z + 20}}

​

Task 1 - Found Guilty of Reason

1. Use forward reasoning to fill in the missing assertions in the following code. Use invertible operations.

{{y > 5 and z > 2}}

x = 4 * y - 3

{{y > 5 and z > 2 and x = 4y - 3}}

y = y - 5

{{-}}

z = z * y

{{P: }}

{{Q: x < 2z + 20}}

​

Task 1 - Found Guilty of Reason

1. Use forward reasoning to fill in the missing assertions in the following code. Use invertible operations.

{{y > 5 and z > 2}}

x = 4 * y - 3

{{y > 5 and z > 2 and x = 4y - 3}}

y = y - 5

{{y + 5 > 5 and z > 2 and x = 4(y + 5) - 3}}

z = z * y

{{P: }}

{{Q: x < 2z + 20}}

​

Task 1 - Found Guilty of Reason

1. Use forward reasoning to fill in the missing assertions in the following code. Use invertible operations.

{{y > 5 and z > 2}}

x = 4 * y - 3

{{y > 5 and z > 2 and x = 4y - 3}}

y = y - 5

{{y + 5 > 5 and z > 2 and x = 4(y + 5) - 3}}

z = z * y

{{P: y + 5 > 5 and z / y > 2 and x = 4(y + 5) - 3}}

{{Q: x < 2z + 20}}

​

Task 1 - Found Guilty of Reason

b) Use forward reasoning to fill in the missing assertions in the following code. Use subscripts or invertible operations.

/*

* Computes the square of (x + 1)

* @param x The number to increment and square

* @return (x + 1)^2

*/

public static int nextSquare(int x) {

int y = x * x;

{{ - }}

y = y + (2 * x);

{{ - }}

y = y + 1;

{{P:}}

return y;

}

Task 1 - Found Guilty of Reason

b) Use forward reasoning to fill in the missing assertions in the following code. Use subscripts or invertible operations.

/*

* Computes the square of (x + 1)

* @param x The number to increment and square

* @return (x + 1)^2

*/

public static int nextSquare(int x) {

int y = x * x;

{{y = x^2}}

y = y + (2 * x);

{{ - }}

y = y + 1;

{{P:}}

return y;

}

Task 1 - Found Guilty of Reason

b) Use forward reasoning to fill in the missing assertions in the following code. Use subscripts or invertible operations.

/*

* Computes the square of (x + 1)

* @param x The number to increment and square

* @return (x + 1)^2

*/

public static int nextSquare(int x) {

int y = x * x;

{{y = x^2}}

y = y + (2 * x);

{{y - 2x = x^2}}

y = y + 1;

{{P:}}

return y;

}

Task 1 - Found Guilty of Reason

b) Use forward reasoning to fill in the missing assertions in the following code. Use subscripts or invertible operations.

/*

* Computes the square of (x + 1)

* @param x The number to increment and square

* @return (x + 1)^2

*/

public static int nextSquare(int x) {

int y = x * x;

{{y = x^2}}

y = y + (2 * x);

{{y - 2x = x^2}}

y = y + 1;

{{P: y - 2x - 1 = x^2}} ←→ {{y = x^2 + 2x + 1}}

return y;

}

Task 2 - Does a Duck Say “Back”?

1. Use backward reasoning to fill in the missing assertions in the following code:

{{P: x < w + 1 and w > 0}}

{{Q:}}

y = 4 * w

{{ - }}

x = x * 2

{{ - }}

z = x - 8

{{z < y}}

​

Task 2 - Does a Duck Say “Back”?

1. Use backward reasoning to fill in the missing assertions in the following code:

{{P: x < w + 1 and w > 0}}

{{Q:}}

y = 4 * w

{{ - }}

x = x * 2

{{x - 8 < y}}

z = x - 8

{{z < y}}

​

Task 2 - Does a Duck Say “Back”?

1. Use backward reasoning to fill in the missing assertions in the following code:

{{P: x < w + 1 and w > 0}}

{{Q:}}

y = 4 * w

{{2x - 8 < y}}

x = x * 2

{{x - 8 < y}}

z = x - 8

{{z < y}}

​

Task 2 - Does a Duck Say “Back”?

1. Use backward reasoning to fill in the missing assertions in the following code:

{{P: x < w + 1 and w > 0}}

{{Q: 2x - 8 < 4w}} ←→ {{x < 2w + 4}}

y = 4 * w

{{2x - 8 < y}}

x = x * 2

{{x - 8 < y}}

z = x - 8

{{z < y}}

​

Task 2 - Does a Duck Say “Back”?

b) Use backward reasoning to fill in the missing assertions in the following code:

{{Q:}}

int b = 2 * c

{{ - }}

c = c - 1

{{ - }}

int a = b + 1

{{a >= c}}

return a;

Task 2 - Does a Duck Say “Back”?

b) Use backward reasoning to fill in the missing assertions in the following code:

{{Q:}}

int b = 2 * c

{{ - }}

c = c - 1

{{b + 1 >= c}}

int a = b + 1

{{a >= c}}

return a;

Task 2 - Does a Duck Say “Back”?

b) Use backward reasoning to fill in the missing assertions in the following code:

{{Q:}}

int b = 2 * c

{{b + 1 >= c - 1}}

c = c - 1

{{b + 1 >= c}}

int a = b + 1

{{a >= c}}

return a;

Task 2 - Does a Duck Say “Back”?

b) Use backward reasoning to fill in the missing assertions in the following code:

{{Q: 2c + 1 >= c - 1}} ←→ {{c >= -2}}

int b = 2 * c

{{b + 1 >= c - 1}}

c = c - 1

{{b + 1 >= c}}

int a = b + 1

{{a >= c}}

return a;

Conditionals – Review

• Reason through “then” and “else” branches independently and combine last assertion of both branches with an “or” at the end
• Prove that each implies post condition by cases
• Note: this is important for your homework!

public static int g(int n) {

{{ }}

int m = 0;

if (n >= 0) {

m = 2 * n + 1;

} else {

m = 0;

}

{{m > n}}

return m;

}

​

{{ }}

int m = 0;

if (n >= 0) {

m = 2 * n + 1;

} else {

m = 0;

}

{{m > n}}

return m;

}

Task 3 - Nothing to be If-ed At

{{0 <= s < len and d >= 0}}

int w;

if (s + d <= len) {

{{ - }}

w = d;

{{P1:}}

} else {

{{ - }}

w = len - s;

{{P2:}}

}

{{ - }}

return w;

​

Task 3 - Nothing to be If-ed At

{{0 <= s < len and d >= 0}}

int w;

if (s + d <= len) {

{{0 <= s < len and d >= 0 and s + d <= len}}

w = d;

{{P1:}}

} else {

{{ - }}

w = len - s;

{{P2:}}

}

{{ - }}

return w;

​

Task 3 - Nothing to be If-ed At

{{0 <= s < len and d >= 0}}

int w;

if (s + d <= len) {

{{0 <= s < len and d >= 0 and s + d <= len}}

w = d;

{{P1: 0 <= s < len and d >= 0 and s + d <= len and w = d}}

} else {

{{ - }}

w = len - s;

{{P2:}}

}

{{ - }}

return w;

​

Task 3 - Nothing to be If-ed At

{{0 <= s < len and d >= 0}}

int w;

if (s + d <= len) {

{{0 <= s < len and d >= 0 and s + d <= len}}

w = d;

{{P1: 0 <= s < len and d >= 0 and s + d <= len and w = d}}

} else {

{{0 <= s < len and d >= 0 and s + d > len}}

w = len - s;

{{P2:}}

}

{{ - }}

return w;

​

Task 3 - Nothing to be If-ed At

{{0 <= s < len and d >= 0}}

int w;

if (s + d <= len) {

{{0 <= s < len and d >= 0 and s + d <= len}}

w = d;

{{P1: 0 <= s < len and d >= 0 and s + d <= len and w = d}}

} else {

{{0 <= s < len and d >= 0 and s + d > len}}

w = len - s;

{{P2: 0 <= s < len and d >= 0 and s + d > len and w = len - s}}

}

{{ - }}

return w;

​

Task 3 - Nothing to be If-ed At

{{0 <= s < len and d >= 0}}

int w;

if (s + d <= len) {

{{0 <= s < len and d >= 0 and s + d <= len}}

w = d;

{{P1: 0 <= s < len and d >= 0 and s + d <= len and w = d}}

} else {

{{0 <= s < len and d >= 0 and s + d > len}}

w = len - s;

{{P2: 0 <= s < len and d >= 0 and s + d > len and w = len - s}}

}

{{P1 or P2}}

return w;

​

Loop Invariant – Review

• Loop invariant must be true every time at the top of the loop
• The first time (before any iterations) and for the beginning of each iteration
• Also true every time at the bottom of the loop
• Meaning it’s true immediately after the loop exits
• During the body of the loop (during S), it isn’t true

​

• Must use “Inv” notation to indicate that it’s not a standard assertion

true!

{{Inv: I}}

while (cond) {

S

}

true!

true!

true!

Question ….

Where is it allowed for a loop invariant not to hold?

​

• before the loop

​

• after the loop

​

• after entering the loop

​

• before exiting the loop

​

• during the code execution inside of the loop

Question ….

Where is it allowed for a loop invariant not to hold?

​

• before the loop

​

• after the loop

​

• after entering the loop

​

• before exiting the loop

​

• during the code execution inside of the loop

Rule: while loop

{{ P }}

{{ Inv: I }}

while (b) {

{{ Inv: I and b }}

body

{{ Inv: I }}

}

{{ Inv: I and not b }}

{{ Q }}

The triple {{ P }} while ... {{ Q }} is valid if three checks pass:

1. {{ P }} implies {{ Inv: I }}.
2. The triple {{ Inv: I and b }} body {{ Inv: I }} is valid.
3. {{ Inv: I and not b }} implies {{ Q }}.

Task 4 - Everybody Loops

In this problem, we will prove the correctness of a method containing a loop that finds the quotient of x divided by 10, i.e., the largest value y such that 10y <= x. To say that y is the largest such value means that any larger value would not satisfy the inequality, i.e., that 10(y + 1) !<= x…

Task 4 - 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: _________________________ }}

{{ Inv: x_0 - 10y = x and x >= 0 }}

while (x >= 10) {

{{ _____________________________ }}

y = y + 1;

{{ _____________________________ }}

x = x - 10;

{{ P3: _________________________ }}

{{ Q2: _________________________ }}

}

{{ P2: _________________________ }}

{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}

return y;

}

​

Task 4 - Everybody Loops

1. Check (1):

Fill in P1 using subscripts, then show that the invariant is true when we get to the top of the loop the first time.

​

{{ x = x_0 and x_0 >= 0 }}

int y = 0;

{{ P1: _________________________ }}

{{ Inv: x_0 - 10y = x and x >= 0 }}

Task 4 - Everybody Loops

1. Check (1):

Fill in P1 using subscripts, then show that the invariant is true when we get to the top of the loop the first time.

​

{{ 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 }}

Task 4 - Everybody Loops

1. Check (1):

Fill in P1 using subscripts, then show that the invariant is true when we get to the top of the loop the first time.

​

{{ 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 4 - Everybody Loops

1. Check (1):

Fill in P1 using subscripts, then show that the invariant is true when we get to the top of the loop the first time.

​

{{ 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, then show that Q1 holds when we

exit the loop.

​

{{ Inv: x_0 - 10y = x and x >= 0 }}

while (x >= 10) {

// Loop body

}

{{ P2: _________________________ }}

{{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}

return y;

​

​

​

Task 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, then show that Q1 holds when we

exit the loop.

​

{{ Inv: x_0 - 10y = x and x >= 0 }}

while (x >= 10) {

// Loop body

}

{{ 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 }}

​

​

​

​

​

Task 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 4 - Everybody Loops

b) Check (3):

Fill in P2 using subscripts, 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 4 - Everybody Loops

c) Check (2):

Fill in Q2 using subscripts (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.

​

{{ Inv: x_0 - 10y = x and x >= 0 }}

while (x >= 10) {

{{ _____________________________ }}

y = y + 1;

{{ _____________________________ }}

x = x - 10;

{{ P3: _________________________ }}

{{ Q2: _________________________ }}

}

​

​

​

Task 4 - Everybody Loops

c) Check (2):

Fill in Q2 using subscripts (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.

​

{{ Inv: x_0 - 10y = x and x >= 0 }}

while (x >= 10) {

{{ _____________________________ }}

y = y + 1;

{{ _____________________________ }}

x = x - 10;

{{ P3: _________________________ }}

{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}

}

​

​

​

Task 4 - Everybody Loops

c) Check (2):

Fill in Q2 using subscripts (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.

​

{{ 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 = x - 10;

{{ P3: _________________________ }}

{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}

}

​

​

​

Task 4 - Everybody Loops

c) Check (2):

Fill in Q2 using subscripts (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.

​

{{ 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_0) = x and x >= 0 and x >= 10 and y = y_0 + 1}}

x = x - 10;

{{ P3: _________________________ }}

{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}

}

​

​

​

Task 4 - Everybody Loops

c) Check (2):

Fill in Q2 using subscripts (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.

​

{{ 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_0) = x and x >= 0 and x >= 10 and y = y_0 + 1}}

x = x - 10;

{{ P3: x_0 - 10(y_0) = x_1 and x_1 >= 0 and x_1 >= 10 and

y = y_0 + 1 and x = x_1 - 10}}

{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}

}

​

​

Task 4 - Everybody Loops

c) Check (2):

Fill in Q2 using subscripts (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_0) = x_1 and x_1 >= 0 and x_1 >= 10 and y = y_0 + 1 and x = x_1 - 10}}

{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}

Task 4 - Everybody Loops

c) Check (2):

{{ P3: x_0 - 10(y_0) = x_1 and x_1 >= 0 and x_1 >= 10 and

y = y_0 + 1 and x = x_1 - 10}}

{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}

To show the first part of Inv, from P3 we know:

x = x_1 - 10 since x = x_1 - 10

= x_0 - 10(y_0) - 10 since x_1 = x_0 - 10(y_0)

= x_0 - 10(y_0 + 1) algebra

= x_0 - 10y since y = y_0 + 1

​

For the second part of Inv, from P3, we know that x₁ >= 10 and x = x₁ - 10. Substituting this:

x = x_1 - 10 since P3(5)

>= 10 - 10 since P3(3)

= 0

Please turn in your halfsheets!

:)