CSE 331: Specifications practice

Question 1: Specification Strength

Consider four possible specifications for a method static int half(int n). You may assume no arithmetic here ever overflows.

Spec A
  @requires 0 <= n
  @return   n / 2, rounded down

Spec B
  @requires 0 <= n
  @return   some h with 2 * h <= n

Spec C
  @return   some h with 2 * h <= n

Spec D
  @requires 0 <= n
  @return   some h with 0 <= h and 2 * h <= n

For each pair, write in its box:

S if the first specification is stronger than the second
W if the first is weaker than the second
I if the two are incomparable

	Answer
AB. A and B
AC. A and C
AD. A and D
BC. B and C
BD. B and D
CD. C and D

AB. A and B

Answer

Answer
S

Stronger: A asks the same as B and promises more.

The preconditions are the same.

Both are 0 <= n.

A's postcondition is stronger.

Both allow only calls with 0 <= n, so compare them on those calls.
A allows one result: n / 2, rounded down.
Twice that is at most n, so B allows it too.
B allows more: for n = 4, B allows 0, and A allows only 2.

An implementation that shows it:

return n / 2 - 1; meets B and not A.
- Where 0 <= n, twice n / 2 is at most n, so twice the result is at most n - 2, so at most n, as B asks.
- For n = 4 it returns 1, and A asks for 2.

The rule: Lecture 2's Stronger and weaker.

AC. A and C

Answer

Answer
I

Incomparable: A asks more than C, but promises more where 0 <= n.

C's precondition is weaker.

C asks nothing; A asks 0 <= n.
So A cannot be stronger than C.

A's postcondition is stronger.

A allows only calls with 0 <= n, so compare them on those calls.
A allows one result: n / 2, rounded down.
Twice that is at most n, so C allows it too.
C allows more: for n = 4, C allows 0, and A allows only 2.
So C cannot be stronger than A either.

Two implementations that show it:

return Math.abs(n) / 2; meets A and not C.
- Where 0 <= n, it returns n / 2, rounded down, as A asks.
- For n = -4 it returns 2, and 2 * 2 <= -4 is false.
return Math.min(n, -1); meets C and not A.
- Where n < 0, it returns n, and 2 * n <= n.
- Where 0 <= n, it returns -1, and 2 * -1 <= n.
- For n = 4 it returns -1, and A asks for 2.

The rule: Lecture 2's Stronger and weaker.

AD. A and D

Answer

Answer
S

Stronger: A asks the same as D and promises more.

The preconditions are the same.

Both are 0 <= n.

A's postcondition is stronger.

Both allow only calls with 0 <= n, so compare them on those calls.
A allows one result: n / 2, rounded down.
That is at least 0, and twice it is at most n, so D allows it too.
D allows more: for n = 4, D allows 0, 1, and 2, and A allows only 2.

An implementation that shows it:

return 0; meets D and not A.
- Where 0 <= n, 0 is at least 0 and 2 * 0 <= n, as D asks.
- For n = 4 it returns 0, and A asks for 2.

The rule: Lecture 2's Stronger and weaker.

BC. B and C

Answer

Answer
W

Weaker: B asks more than C and promises the same.

C's precondition is weaker.

C asks nothing; B asks 0 <= n.

The postconditions are the same.

Both are 2 * h <= n.

An implementation that shows it:

return Math.abs(n) / 2; meets B and not C.
- Where 0 <= n, it returns n / 2, and twice that is at most n, as B asks.
- For n = -4 it returns 2, and 2 * 2 <= -4 is false.

The rule: Lecture 2's Stronger and weaker.

BD. B and D

Answer

Answer
W

Weaker: B asks the same as D and promises less.

The preconditions are the same.

Both are 0 <= n.

D's postcondition is stronger.

Both allow only calls with 0 <= n, so compare them on those calls.
D's postcondition adds 0 <= h to B's, so every result D allows, B allows too.
B allows more: for n = 4, B allows -1, and D does not.
- 0 <= n is about the argument, not the result.
- 2 * h <= n is an inequality, and -1 meets it: 2 * -1 <= 4.

An implementation that shows it:

return n / 2 - 1; meets B and not D.
- Where 0 <= n, twice n / 2 is at most n, so twice the result is at most n - 2, so at most n, as B asks.
- For n = 0 it returns -1, and D asks for 0 <= h.

The rule: Lecture 2's Stronger and weaker.

CD. C and D

Answer

Answer
I

Incomparable: C asks less than D, but promises less where 0 <= n.

C's precondition is weaker.

C asks nothing; D asks 0 <= n.
So D cannot be stronger than C.

D's postcondition is stronger.

D allows only calls with 0 <= n, so compare them on those calls.
D's postcondition adds 0 <= h to C's, so every result D allows, C allows too.
C allows more: for n = 4, C allows -1, and D does not.
- 0 <= n is about the argument, not the result.
- 2 * h <= n is an inequality, and -1 meets it: 2 * -1 <= 4.
So C cannot be stronger than D either.

Two implementations that show it:

return Math.min(n, -1); meets C and not D.
- Where n < 0, it returns n, and 2 * n <= n.
- Where 0 <= n, it returns -1, and 2 * -1 <= n.
- For n = 0 it returns -1, and D asks for 0 <= h.
return Math.abs(n) / 2; meets D and not C.
- Where 0 <= n, it returns n / 2: at least 0, and twice it is at most n, as D asks.
- For n = -4 it returns 2, and 2 * 2 <= -4 is false.

The rule: Lecture 2's Stronger and weaker.

Question 2: Specification Strength

Consider four possible specifications for a method static int root(int x). Call x a perfect square when x = k * k for some integer k; a perfect square is therefore at least 0. You may assume no arithmetic here ever overflows.

Spec A
  @requires x is a perfect square
  @return   an integer y with y * y = x

Spec B
  @requires x is a perfect square
  @return   the integer y with 0 <= y and y * y = x

Spec C
  @return   0 if x < 0, and otherwise the largest integer y
            with y * y <= x

Spec D
  @requires 0 <= x
  @return   an integer y with 0 <= y and y * y <= x

For each pair, write in its box:

S if the first specification is stronger than the second
W if the first is weaker than the second
I if the two are incomparable

	Answer
AB. A and B
AC. A and C
AD. A and D
BC. B and C
BD. B and D
CD. C and D

AB. A and B

Answer

Answer
W

Weaker: A asks the same as B and promises less.

The preconditions are the same.

Both ask that x be a perfect square.

B's postcondition is stronger.

Both allow only calls where x is a perfect square, so compare them on those calls.
B allows one result: the root that is at least 0.
That result squares to x, so A allows it too.
A allows more: for x = 4, A allows -2, and B does not.

An implementation that shows it:

One that returns the root that is at most 0 when x is a perfect square meets A and not B.
- Where x is a perfect square, its result squares to x, as A asks.
- For x = 4 it returns -2, and B asks for 2.

The rule: Lecture 2's Stronger and weaker.

AC. A and C

Answer

Answer
W

Weaker: A asks more than C and promises less.

C's precondition is weaker.

C asks nothing; A asks that x be a perfect square.

C's postcondition is stronger.

A allows only calls where x is a perfect square, so compare them on those calls.
C allows one result: the largest y with y * y <= x.
On a perfect square, that is the root that is at least 0.
It squares to x, so A allows it too.
A allows more: for x = 4, A allows -2, and C does not.

An implementation that shows it:

One that returns the root that is at most 0 when x is a perfect square meets A and not C.
- Where x is a perfect square, its result squares to x, as A asks.
- For x = 4 it returns -2, and C asks for 2.

The rule: Lecture 2's Stronger and weaker.

AD. A and D

Answer

Answer
I

Incomparable: D asks less than A, but allows a result A forbids.

D's precondition is weaker.

D asks 0 <= x; A asks that x be a perfect square, which is in particular at least 0.
So A cannot be stronger than D.

D's postcondition allows a result A forbids.

A allows only calls where x is a perfect square, so compare them on those calls.
For x = 4, D allows 0, and A asks for y * y = 4.
So D cannot be stronger than A either.

Two implementations that show it:

return 0; meets D and not A.
- Where 0 <= x, 0 is at least 0 and 0 * 0 <= x, as D asks.
- For x = 4 it returns 0, and A asks for 2 or -2.
One that returns the root that is at least 0 when x is a perfect square, and -1 otherwise, meets A and not D.
- Where x is a perfect square, its result squares to x, as A asks.
- For x = 2 it returns -1, and D asks for 0 <= y.

The rule: Lecture 2's Stronger and weaker.

BC. B and C

Answer

Answer
W

Weaker: B asks more than C and promises the same on the calls B allows.

C's precondition is weaker.

C asks nothing; B asks that x be a perfect square.

The postconditions agree on the calls B allows.

B allows only calls where x is a perfect square, so compare them on those calls.
There, the largest y with y * y <= x is the root that is at least 0: C's one result is B's one result.
C promises more only where x is not a perfect square, which B's precondition rules out.

An implementation that shows it:

One that returns the root that is at least 0 when x is a perfect square, and -1 otherwise, meets B and not C.
- Where x is a perfect square, it does what B asks.
- For x = 2 it returns -1, and C asks for 1.

The rule: Lecture 2's Stronger and weaker.

BD. B and D

Answer

Answer
I

Incomparable: D asks less than B, but promises less on the calls B allows.

D's precondition is weaker.

D asks 0 <= x; B asks that x be a perfect square, which is in particular at least 0.
So B cannot be stronger than D.

B's postcondition is stronger.

B allows only calls where x is a perfect square, so compare them on those calls.
B allows one result: the root that is at least 0.
It is at least 0 and squares to x, so D allows it too.
D allows more: for x = 4, D allows 0, 1, and 2, and B allows only 2.
So D cannot be stronger than B either.

Two implementations that show it:

return 0; meets D and not B.
- Where 0 <= x, 0 is at least 0 and 0 * 0 <= x, as D asks.
- For x = 4 it returns 0, and B asks for 2.
One that returns the root that is at least 0 when x is a perfect square, and -1 otherwise, meets B and not D.
- Where x is a perfect square, it does what B asks.
- For x = 2 it returns -1, and D asks for 0 <= y.

The rule: Lecture 2's Stronger and weaker.

CD. C and D

Answer

Answer
S

Stronger: C asks less than D and promises more.

C's precondition is weaker.

C asks nothing; D asks 0 <= x.

C's postcondition is stronger.

D allows only calls with 0 <= x, so compare them on those calls.
C allows one result: the largest y with y * y <= x.
It is at least 0, since 0 * 0 <= x, and it squares to at most x, so D allows it too.
D allows more: for x = 4, D allows 0, 1, and 2, and C allows only 2.

An implementation that shows it:

return 0; meets D and not C.
- Where 0 <= x, 0 is at least 0 and 0 * 0 <= x, as D asks.
- For x = 4 it returns 0, and C asks for 2.

The rule: Lecture 2's Stronger and weaker.