CSE 331�Software Design & Implementation
Spring 2026
Section 1 – Specifications
Review - Abstraction
Review – Specification Types
• Imperative specification says how to calculate the answer
• Declarative specification says what the answer looks like
Question - Specification Types
What type is each of these specs?:
Question - Specification Types
What type is each of these specs?:
Question - Specification Types
What type is each of these specs?:
New! Stronger vs Weaker
An assertion is stronger if and only if it holds in a subset of states
Below, Q2 is the stronger assertion as knowing Q2 is true tells us that Q1 is true. However, knowing Q1 is true doesn’t tell us Q2 is true.
Review – Specifications
A specification consists of two parts:
Precondition: Allowed inputs
Postcondition: Allowed outputs
A specification is stronger when it has less restrictive inputs and more restrictive outputs. In other words, strong specifications have more guarantees for a larger set of inputs.
Documenting Methods w/ JavaDoc
*Note: @requires is unique to 331
JavaDoc comments use “tags” to describe what methods do
/**
* High level description of what function does
* @param a + What "a" represents + any conditions about a
* @requires Rules about multiple params
* @returns Detailed description of return value
* @throws Condition when errors will be thrown
*/
Specification Strength: Immutable
Specification Strength: Immutable
Question - Specifications
Which of the two specs is stronger?:
/** Returns the square root of a given number x
* @requires x >= 0
* @return the integer y such that y^2 = x
*/
Or
/** Returns the square root of a given number x
* @requires x >= 0
* @return the integer y such that y^2 = x and y >= 0
*/
Question - Specifications
Which of the two specs is stronger?:
/** Returns the square root of a given number x
* @requires x >= 0
* @return the integer y such that y^2 = x
*/
Or
/** Returns the square root of a given number x
* @requires x >= 0
* @return the integer y such that y^2 = x and y >= 0
*/
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
a) “price > 0 and items is not null” or “items is not null”
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
a) “price > 0 and items is not null” or “items is not null”
“price > 0 and items is not null” is the stronger assertion
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
b) “price > 0” or “price >= 0”
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
b) “price > 0” or “price >= 0”
“price > 0” is the stronger assertion because if price > 0, we know that price >= 0 must be true as well.
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
c) “items is an array” or “items is a sorted array”
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
c) “items is an array” or “items is a sorted array”
“items is a sorted array” is the stronger assertion.
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
d) “price > 0” or “items is not null”
Task 1
Suppose price is an integer and items is an array. Determine whether each pair of assertions is comparable, and if they are, state which is stronger and which is weaker. Recall that a stronger assertion implies a weaker assertion, so if the stronger one is true, the weaker one is also true.
d) “price > 0” or “items is not null”
These two are incomparable!
Task 2
We plan to provide the following method:
/** Returns the best menu item for the given price.� * …� */�public static MenuItem findBest(int price, MenuItem[] items);
To do so, we need to fill in the rest of the specification. For example, we need to explain exactly which item will be returned. The term “best” is far too vague.
We are considering the following alternatives:
Task 2
@requires price > 0 and items is not null // Spec A�@return an item T in items with T.price <= price <= T.price + 0.5 or null if none exists
@requires items is not null // Spec B�@throws IllegalArgumentException if price <= 0�@return an item T in items with T.price <= price <= T.price + 0.5 or null if none exists
@requires price > 0 and items is not null // Spec C�@return the item in items whose price is closest to the given price but not more than the given price or null if none exists
@requires price > 0 // Spec D�@throws NullPointerException if items is null�@return the item in items whose price is closest to the given price but not more than the given price or null if none exists
@requires price > 0 // Spec E�@return an item T in items with T.price <= price <= T.price + 0.5 or null if none exists or if items is null
Task 2a
| A | B | C | D | E |
A | X | | | | |
B | | X | | | |
C | | | X | | |
D | | | | X | |
E | | | | | X |
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | | | |
B | S | X | | | |
C | | | X | | |
D | | | | X | |
E | | | | | X |
A is weaker than B as A has more restrictive inputs (price > 0)
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | - | | |
B | S | X | | | |
C | - | | X | | |
D | | | | X | |
E | | | | | X |
A & C are incomparable (have different but incomparable postconditions)
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | - | - | |
B | S | X | | | |
C | - | | X | | |
D | - | | | X | |
E | | | | | X |
A & D are incomparable (D has a weaker precondition, but they have different but incomparable postconditions)
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | - | - | W |
B | S | X | | | |
C | - | | X | | |
D | - | | | X | |
E | S | | | | X |
A is also weaker than E as A has more restrictive inputs (items is not null) and less restrictive outputs (null if items is null).
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | - | - | W |
B | S | X | - | - | - |
C | - | - | X | | |
D | - | - | | X | |
E | S | - | | | X |
B is incomparable with C & D because they have incomparable postconditions
B is incomparable with E because they have incomparable preconditions
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | - | - | W |
B | S | X | - | - | - |
C | - | - | X | W | - |
D | - | - | S | X | |
E | S | - | - | | X |
C is weaker than D as C has more restrictive inputs (items is not null). While D throws an exception on that same input, it still “accepts” the input and actually has more guarantees (more restrictive output) as a result.
C & E are incomparable because they have incomparable postconditions.
Task 2a
Using the specs listed, fill in the following table explaining the relationships between each pair of specifications. Write an “S” if the spec on left (the row) is stronger than the spec on top (the column), a “W” if the left spec is weaker, and “-” if the specs are incomparable.
| A | B | C | D | E |
A | X | W | - | - | W |
B | S | X | - | - | - |
C | - | - | X | W | - |
D | - | - | S | X | - |
E | S | - | - | - | X |
D & E are incomparable because they have incomparable postconditions.
Task 2b
b) Now consider a new pair of precondition and postcondition behaviors:
@requires price > 0
@return an item T in items with T.price <= price <= T.price + 0.5
This specification is not sensible, what is wrong with it? Why shouldn’t we use it?
Task 2b
b) Now consider a new pair of precondition and postcondition behaviors:
@requires price > 0
@return an item T in items with T.price <= price <= T.price + 0.5
This specification is not sensible, what is wrong with it? Why shouldn’t we use it?
The specification does not describe what should happen if/when items is null. This is a problem because a client cannot effectively use a method if they do not know what happens in some cases.
Task 3a
For each of the following implementations, state which of the specifications it satisfies. If it does not satisfy some specification, explain (in as few words as possible) why it does not.
public static MenuItem findBest(int price, MenuItem[] items) {
if (price <= 0)
throw new IllegalArgumentException("bad price");
for (int i = 0; i < items.length; i++) {
if (items[i].price <= price && price <= items[i].price + 0.5)
return items[i];
}
return null;
}
Task 3a
For each of the following implementations, state which of the specifications it satisfies. If it does not satisfy some specification, explain (in as few words as possible) why it does not.
public static MenuItem findBest(int price, MenuItem[] items) {
if (price <= 0)
throw new IllegalArgumentException("bad price");
for (int i = 0; i < items.length; i++) {
if (items[i].price <= price && price <= items[i].price + 0.5)
return items[i];
}
return null;
}
A & B.
C & D are not satisfied since the item returned may not be the one nearest below in price.
E is not satisfied since a NullPointerException is thrown instead of returning null when items is null.
Task 3b
For each of the following implementations, state which of the specifications it satisfies. If it does not satisfy some specification, explain (in as few words as possible) why it does not.
public static MenuItem findBest(int price, MenuItem[] items) {
Arrays.sort(items); // puts items in order by increasing price
MenuItem best = null;
for (int i = 0; i < items.length; i++) {
if (items[i].price <= price)
best = items[i];
}
return best;
}
Task 3b
For each of the following implementations, state which of the specifications it satisfies. If it does not satisfy some specification, explain (in as few words as possible) why it does not.
public static MenuItem findBest(int price, MenuItem[] items) {
Arrays.sort(items); // puts items in order by increasing price
MenuItem best = null;
for (int i = 0; i < items.length; i++) {
if (items[i].price <= price)
best = items[i];
}
return best;
}
C & D.
A & B & E are not valid since the return may not be within the required price range
Task 3c
For each of the following implementations, state which of the specifications it satisfies. If it does not satisfy some specification, explain (in as few words as possible) why it does not.
public static MenuItem findBest(int price, MenuItem[] items) {
if (items == null)
return null;
if (price <= 0)
throw new IllegalArgumentException("bad price");
for (int i = 0; i < items.length; i++) {
if (items[i].price <= price && price <= items[i].price + 0.5)
return items[i];
}
return null;
}
Task 3c
For each of the following implementations, state which of the specifications it satisfies. If it does not satisfy some specification, explain (in as few words as possible) why it does not.
A, B, & E.
C & D are not satisfied since the item returned may not be the one nearest below in price.
public static MenuItem findBest(int price, MenuItem[] items) {
if (items == null)
return null;
if (price <= 0)
throw new IllegalArgumentException("bad price");
for (int i = 0; i < items.length; i++) {
if (items[i].price <= price && price <= items[i].price + 0.5)
return items[i];
}
return null;
}