CSE 331�Software Design & Implementation

​

Spring 2026

Section 3 – Floyd Logic

Administrivia

HW2 released tonight - Due next Wed (7/15) 11:59pm

​

​

​

2

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.

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

• Invertible operations
• When gathering and updating facts, you should put the value in terms of the old value
• This is much more readable but not everything can be represented
• Ex: Integer division

​

• Subscripts
• You’ll continually gather and append new facts with subscripts to represent them
• Gets messy quickly in complex or strange programs
• The extra detail helps us represent everything

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

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

y = 3 * x;

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

z = y + 1

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

Unless specified, we allow both inverted operations and subscripts!

does not simplify assertions early or drop variable relationships

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:

• 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.

Task 1 - Found Guilty of Reason

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

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

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

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

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

/*

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

/*

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

/*

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

/*

* 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”?

• 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

{{ - }}

int 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

{{ - }}

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

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

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

​

End