1 of 39

CSE 331�Software Design & Implementation

Spring 2026

Section 1 – Specifications

2 of 39

Review - Abstraction

  • Hides unnecessary details from clients via specification
  • Creates an Abstraction Barrier between clients and implementers
    • Implementers promise that the code follows the specification
    • Clients promise not to rely on details outside the specification

3 of 39

Review – Specification Types

Imperative specification says how to calculate the answer

  • Gives the exact steps to get the answer
  • Just have to translate math to code
  • Ex: Absolute value: |x| = x if x ≥ 0 and –x otherwise

Declarative specification says what the answer looks like

  • Does not say how to calculate it
  • Up to us to ensure that our code satisfies the spec
  • Ex: Absolute value: returns the non-negative distance from 0 to x

4 of 39

Question - Specification Types

What type is each of these specs?:

  • Steps to calculate the square of a number n: multiply n by itself, n * n.
  • Declarative
  • Imperative

  • Return a number, such that this number is the same value as the square of n
  • Declarative
  • Imperative

5 of 39

Question - Specification Types

What type is each of these specs?:

  • Steps to calculate the square of a number n: multiply n by itself, n * n.
  • Declarative
  • Imperative

  • Return a number, such that this number is the same value as the square of n
  • Declarative
  • Imperative

6 of 39

Question - Specification Types

What type is each of these specs?:

  • Steps to calculate the square of a number n: multiply n by itself, n * n.
  • Declarative
  • Imperative

  • Return a number, such that this number is the same value as the square of n
  • Declarative
  • Imperative

7 of 39

New! Stronger vs Weaker

An assertion is stronger if and only if it holds in a subset of states

  • A stronger assertion implies the weaker one
  • This means that if the stronger assertion is true, then the weaker assertion must also be true.

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.

8 of 39

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.

9 of 39

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

*/

10 of 39

Specification Strength: Immutable

  • Accepting more generic @params increases specification strength (same params w/ less restrictions)
    • We’ll talk about this later with generics

  • Adding more to @requires decreases specification strength
    • Strengthens the precondition (takes in less inputs)
    • Ex: param List lst must be sorted is more restrictive = stronger precondition = weaker spec than no requirement about order

11 of 39

Specification Strength: Immutable

  • Adding more to @returns increases specification strength
    • Strengthens the postcondition

  • @throws still specifies behavior, so it is stronger than @requires
    • Still accepts that input and defines the behavior for it

12 of 39

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

*/

13 of 39

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

*/

14 of 39

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

15 of 39

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

16 of 39

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

17 of 39

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.

18 of 39

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

19 of 39

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.

20 of 39

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

21 of 39

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!

22 of 39

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:

23 of 39

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

24 of 39

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.

25 of 39

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)

26 of 39

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)

27 of 39

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)

28 of 39

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

29 of 39

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

30 of 39

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.

31 of 39

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.

32 of 39

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?

33 of 39

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.

34 of 39

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;

}

35 of 39

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.

36 of 39

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;

}

37 of 39

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

38 of 39

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;

}

39 of 39

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;

}