CSE 331�Software Design & Implementation
Autumn 2026
Section 1 – Specifications
Welcome!
Homework Cycle
Review - Abstraction
Documenting Methods w/ JavaDoc
*Note: @requires, @modifies, and @effects are all 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
*/
For methods that mutate variables/state, will have 2 additional tags to describe mutation
* @modifies states what could be mutated by function
* @effects Detailed description of guaranteed changes
Spec/Impl Lecture Exercise
// Spec B
// @requires 0 <= lo <= hi <= a.length
// @returns the *smallest* index i with lo <= i < hi and a[i] == x,
// or -1 if no such index exists
// Spec D
// @requires 0 <= lo <= hi <= a.length
// @returns *some* index i with lo <= i < hi and a[i] == x,
// or -1 if no such index exists
// Impl 1
public static int indexOf(int[] a, int lo, int hi, int x) {
for (int i = lo; i < hi; i++) {
if (a[i] == x) {
return i;
}
}
return -1;
}
When spec B is satisfied, spec D is also satisfied!
(311 implication)
What do you notice about these two specs and Impl 1?
Review: Stronger vs Weaker Assertions
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: Stronger vs Weaker Specs
P2
P1
precondition
postcondition
Q1
Q2
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
*/
Specification Strength: Precondition
Specification Strength: Postcondition
New Notation for Task 1 & 2
We use the notation a[i..j] to refer to the elements of an array a from index i (inclusive) to j (exclusive). So a[0..n] is the elements of a at indices 0, 1, ..., n-1.
Task 1: Spec Comparisons
| 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 2: Mutable Spec/Impl Satisfaction
We use the notation a[i..j] to refer to the elements of an array a from index i (inclusive) to j (exclusive). So a[0..n] is the elements of a at indices 0, 1, ..., n-1.
Task 2: Mutable Spec/Impl Satisfaction
This is the common prefix of each spec.��/**
* Removes x from the prefix a[0..n] (but see below for details)
*
* @param a the non-null array to remove from
* @param n the length of the prefix
* @param x the value to remove
* @requires 0 <= n <= a.length
* @modifies a
*/
Task 2: Mutable Spec/Impl Satisfaction
// Spec A
// @effects if the first occurrence of x in a[0..n] is at index i,
// then the new values in a[0..n-1] will be the old values of a[0..i]
// followed by the old values of a[i+1..n], and the new value of a[n-1]
// is unspecified. else, if x does not occur in a[0..n], leaves a unchanged;
// @return n - 1 if x was removed, else n
// Spec B
// @effects if x does not occur in a[0..n], leaves a unchanged;
// otherwise, the new values in a[0..n-1] are a possibly reordered version
// of the old values of a[0..n] with one fewer occurrence of x,
// and the new value of a[n-1] is unspecified
// @return n - 1 if x was removed, else n
Task 2: Mutable Spec/Impl Satisfaction
// Spec C
// @effects if x does not occur in a[0..n], leaves a unchanged;
// otherwise, if x occurs k > 0 times in a[0..n], then remove all k
// occurrences of x, leaving remaining elements in the same relative
// order as before; the new value of elements in a[n-k..n] is unspecified
// @return n - k
// Spec D
// @requires a[0..n] contains no duplicates
// @effects if x does not occur in a[0..n], leaves a unchanged;
// otherwise, if x occurs in a[0..n] at index i, then the new values
// in a[0..n-1] will be the old values of a[0..i] followed by the
// old values of a[i+1..n], and the new value of a[n-1] is unspecified.
// @return n - 1 if x was removed, else n
Task 2: Implementation 1
// Impl 1
int w = 0;
for (int r = 0; r < n; r++) {
if (a[r] != x) {
a[w] = a[r];
w++;
}
}
return w;
Task 2: Implementation 2
// Impl 2
for (int i = 0; i < n; i++) {
if (a[i] == x) {
for (int k = i; k < n - 1; k++) {
a[k] = a[k + 1];
}
return n - 1;
}
}
return n;
Task 2: Implementation 3
// Impl 3
for (int i = n - 1; i >= 0; i--) {
if (a[i] == x) {
for (int k = i; k < n - 1; k++) {
a[k] = a[k + 1];
}
return n - 1;
}
}
return n;
Task 2: Implementation 4
// Impl 4
for (int i = 0; i < n; i++) {
if (a[i] == x) {
a[i] = a[n - 1];
return n - 1;
}
}
return n;
End
Please turn in your half sheets to us as you leave!!!!