3 of 61

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

4 of 61

Forward Reasoning Error Example

x = x + 1;

y = 3 * x;

z = y + 1;

What’s wrong with these assertions?

Drops this assertion

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

5 of 61

Corrected Forward Reasoning Example

x = x + 1;

y = 3 * x;

z = y + 1

Unless specified, we allow both inverted operations and subscripts!

does not simplify assertions early or drop variable relationships

6 of 61

Backward Reasoning – Review

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

7 of 61

Forward & Backward General Rules

Forward Reasoning:

After each line of code update variables in assertions based on how they they were changed by the line of code

Backward Reasoning:

As you work your way up the code directly substitute how variables are modified in the code into your assertions

General:

Do not substitute or drop assertions
Know how to both invert an operation and use subscripts! We may ask you to do one and not the other.

8 of 61

Task 1 - Found Guilty of Reason

Use forward reasoning to fill in the missing assertions in the following code:

x = 4 * y - 3

y = y - 5

z = z * y

9 of 61

Task 1 - Found Guilty of Reason

Use forward reasoning to fill in the missing assertions in the following code:

x = 4 * y - 3

y = y - 5

z = z * y

10 of 61

Task 1 - Found Guilty of Reason

Use forward reasoning to fill in the missing assertions in the following code:

x = 4 * y - 3

y = y - 5

z = z * y

11 of 61

Task 1 - Found Guilty of Reason

Use forward reasoning to fill in the missing assertions in the following code:

x = 4 * y - 3

y = y - 5

z = z * y

12 of 61

Task 1 - Found Guilty of Reason

b) Show that the code is correct by explaining how P implies Q

13 of 61

Task 1 - Found Guilty of Reason

b) Show that the code is correct by explaining how P implies Q

x = 4y + 17 (since x = 4(y + 5) - 3)

< 2z + 17 (since z > 2y because y > 0)

< 2z + 20

Alternate solution: We know that x = 4(y + 5) - 3 = 4y + 20 - 3 = 4y + 17. Next, we can rewrite z / y > 2 into z > 2y since we know that y > 0 (and therefore multiplying both sides by y doesn't flip the sign). We can then substitute into our original equation that x < 2z + 17. Finally, we know that 17 < 20 so x < 2z + 17. Therefore, Q holds.

14 of 61

Task 1 - Found Guilty of Reason

c) Use forward reasoning to fill in the missing assertions in the following code:

* 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;

return y;

}

15 of 61

Task 1 - Found Guilty of Reason

c) Use forward reasoning to fill in the missing assertions in the following code:

* 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;

return y;

}

16 of 61

Task 1 - Found Guilty of Reason

c) Use forward reasoning to fill in the missing assertions in the following code:

* 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;

return y;

}

17 of 61

Task 1 - Found Guilty of Reason

c) Use forward reasoning to fill in the missing assertions in the following code:

* 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;

return y;

}

18 of 61

Task 1 - Found Guilty of Reason

d) Show that the code is correct by explaining how P implies the postcondition:

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

19 of 61

Task 1 - Found Guilty of Reason

d) Show that the code is correct by explaining how P implies the postcondition:

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

y = x² + 2x + 1 since y = x² + 2x + 1

= (x + 1)²

Alternate solution: We know that y = x² + 2x +1 which we can rewrite using algebra that y = (x + 1)². Therefore, Q holds.

20 of 61

Task 2 - Does a Duck Say “Back”?

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

y = 4 * w

x = x * 2

z = x - 8

21 of 61

Task 2 - Does a Duck Say “Back”?

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

y = 4 * w

x = x * 2

z = x - 8

22 of 61

Task 2 - Does a Duck Say “Back”?

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

y = 4 * w

x = x * 2

z = x - 8

23 of 61

Task 2 - Does a Duck Say “Back”?

b) Show P implies Q

We can see Q holds:

x < w + 1

< 2w + 1 (w > 0)

< 2w + 4

Alternate solution: Alternate solution: We know that x < w + 1. Since w > 0, we know that w < 2w, and w < 2w + 3. Thus, x < w + 1 < 2w + 4.

24 of 61

Task 2 - Does a Duck Say “Back”?

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

// Performs a simple calculation on c

// @param c The input integer

// @requires c >= 0

// @return an integer >= c

public static int calculation(int c) {

int b = 2 * c

c = c - 1

int a = b + 1

return a;

}

25 of 61

Task 2 - Does a Duck Say “Back”?

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

// Performs a simple calculation on c

// @param c The input integer

// @requires c >= 0

// @return an integer >= c

public static int calculation(int c) {

int b = 2 * c

c = c - 1

int a = b + 1

return a;

}

26 of 61

Task 2 - Does a Duck Say “Back”?

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

// Performs a simple calculation on c

// @param c The input integer

// @requires c >= 0

// @return an integer >= c

public static int calculation(int c) {

int b = 2 * c

c = c - 1

int a = b + 1

return a;

}

27 of 61

Task 2 - Does a Duck Say “Back”?

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

// Performs a simple calculation on c

// @param c The input integer

// @requires c >= 0

// @return an integer >= c

public static int calculation(int c) {

int b = 2 * c

c = c - 1

int a = b + 1

return a;

}

28 of 61

Task 2 - Does a Duck Say “Back”?

d) Show how P implies Q

We can see that Q holds since c >= 0 >= -2.

29 of 61

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;

}

return m;

}

int m = 0;

if (n >= 0) {

m = 2 * n + 1;

} else {

m = 0;

}

return m;

}

30 of 61

Task 3 - Nothing to be If-ed At

Use forward reasoning to fill in the assertion

// Calculates a safe substring length starting from a given index

// @param start The starting index of the substring

// @param desired The desired substring length

// @param len The total length of the original string

// @requires 0 <= start < len and desired >= 0

// @return A window size such that start + window <= len

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

} else {

window = len - start;

}

return window;

}

31 of 61

Task 3 - Nothing to be If-ed At

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

} else {

window = len - start;

}

return window;

}

32 of 61

Task 3 - Nothing to be If-ed At

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

} else {

window = len - start;

}

return window;

}

33 of 61

Task 3 - Nothing to be If-ed At

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

{{P1: 0 <= start < len and desired >= 0 and start + desired <= len and window = desired}}

} else {

window = len - start;

}

return window;

}

34 of 61

Task 3 - Nothing to be If-ed At

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

{{P1: 0 <= start < len and desired >= 0 and start + desired <= len and window = desired}}

} else {

window = len - start;

}

return window;

}

35 of 61

Task 3 - Nothing to be If-ed At

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

{{P1: 0 <= start < len and desired >= 0 and start + desired <= len and window = desired}}

} else {

window = len - start;

{{P2: 0 <= start < len and desired >= 0 and start + desired > len and window = len - start}}

}

return window;

}

36 of 61

Task 3 - Nothing to be If-ed At

public static int calcWindow(int start, int desired, int len) {

int window;

if (start + desired <= len) {

window = desired;

{{P1: 0 <= start < len and desired >= 0 and start + desired <= len and window = desired}}

} else {

window = len - start;

{{P2: 0 <= start < len and desired >= 0 and start + desired > len and window = len - start}}

}

return window;

}

37 of 61

Task 3 - Nothing to be If-ed At

The postcondition is “start + window <= len” and we know that “P1 or P2" is true. We will show that the postcondition holds in general:

Suppose P1 is true. We can see:

start + window = start + desired since window = desired

<= len since start + window <= len

Suppose P2 is true. We can see:

start + window = start + (len - start) since window = len - start

= len

<= len

Since these cases are exhaustive and we have shown that in either case the postcondition holds, we have proven that the postcondition holds in general.

38 of 61

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!

while (cond) {

}

true!

39 of 61

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

40 of 61

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

41 of 61

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…

42 of 61

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

int y = 0;

while (x >= 10) {

y = y + 1;

x = x - 10;

}

return y;

}

43 of 61

Task 4 - Everybody Loops

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

int y = 0;

44 of 61

Task 4 - Everybody Loops

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

int y = 0;

45 of 61

Task 4 - Everybody Loops

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

int y = 0;

The first part of the invariant holds

x_0 - 10y = x - 10y since x = x_0

= x since y = 0

46 of 61

Task 4 - Everybody Loops

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

int y = 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

47 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

while (x >= 10) {

// Loop body

}

return y;

48 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

while (x >= 10) {

// Loop body

}

return y;

49 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

50 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

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

51 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

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

52 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

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

53 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

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

54 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

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)

55 of 61

Task 4 - Everybody Loops

b) Fill in P2, then show that Q1 holds when we exit the loop.

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.

56 of 61

Task 4 - Everybody Loops

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.

while (x >= 10) {

y = y + 1;

x = x - 10;

}

57 of 61

Task 4 - Everybody Loops

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.

while (x >= 10) {

y = y + 1;

x = x - 10;

}

58 of 61

Task 4 - Everybody Loops

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.

while (x >= 10) {

y = y + 1;

x = x - 10;

}

59 of 61

Task 4 - Everybody Loops

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.

while (x >= 10) {

y = y + 1;

x = x - 10;

}

60 of 61

Task 4 - Everybody Loops

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.

while (x >= 10) {

y = y + 1;

x = x - 10;

{{ P3: x_0 - 10(y - 1) = x + 10 and x + 10 >= 0 and x + 10 >= 10 }}

}

61 of 61

Task 4 - Everybody Loops

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

We must show P3 implies the invariant:

From P3, we know that x₀ - 10(y - 1) = x + 10. Simplifying this:

x₀ - 10y + 10 = x + 10

x₀ - 10y = x

Also from P3, we know x + 10 >= 10. Subtracting 10 from both sides gives us x >= 0. Thus, the invariant holds.