Software Specifications: Strength and Style Guide

Posted on Sep 4, 2024 in Computers

Exam #1

In Class on Thursday 3/3

  • Crib sheet allowed/encouraged (double-sided 8.5″x11″ sheet of paper or two single-sided 8.5″x11″ sheets of paper) (this crib sheet can include anything at all)
  • Practice Exam available (skip last question)

Homework 1 Solutions

8. { x + 5 < y } whoops x = x + 5 to be corrected { x < y }

9. { x > y }
z = x - y // use forward reasoning
{ z > 0 }

Specification

Need to identify:

  • Precondition
    • requires: Spells out constraints on the client/user of this method.
  • Postcondition
    • modifies: Identifies objects (typically parameters) that may be modified by this method. Any object not listed under this clause is guaranteed to remain untouched.
    • effects: Describes the final state of modified objects.
    • returns: Describes return value(s).
    • throws: Lists out possible exceptions.

Specification Style

For a method call, we’re interested in its side effects (i.e., the effects (and modifies) clause) or its return value

  • It is generally considered “bad style” to have both effects and returns for a method
  • But there are exceptions (e.g., removing an element from a list)

Aside: Specifications and Data Types

In statically typed languages (e.g., C, C++, Java), the type signature is a form of specification

List add( List l1, List l2 )

In dynamically typed languages (e.g., Python, JavaScript), there is no type signature

def add(l1,l2):
  i = 0
  res = []
  for j in l1: res.append(j+l2[i]); i=i+1
  return res

Specifications should be:

  • Concise
  • Informative
  • Precise
  • Specific (strong) enough to make guarantees
  • General (weak) enough to allow for efficient implementation
  • Too weak of a specification imposes too many preconditions and/or gives too few guarantees
  • Too strong of a specification imposes too few preconditions and/or gives too many guarantees
    • The burden is on the implementation side — e.g., is input sorted? (which hinder efficiency of the implementation)

Specification Strength

This provides a means of comparing specifications

Spec A is stronger than Spec B (i.e., A > B)

  • For every implementation I, “I satisfies A” implies “I satisfies B”
  • For every client/user C, “C meets the obligations of B” implies “C meets the obligations of A”
  • A weaker specification is easier to satisfy (and therefore easier to implement)
  • A stronger specification is easier for clients to use (and therefore more difficult to implement and less efficient)

int find( int[] a, int value ) {
  for ( int i = 0 ; i < a.length ; i++ ) { if ( a[i] == value ) return i; }
  return -1;
}

Specification A:
requires: a is non-null and value occurs in a
returns: the smallest index i such that a[i]=value

Specification B:
requires: a is non-null and value occurs in a
returns: index i such that a[i]=value

  • The find() method satisfies both Spec A and Spec B
  • Spec A is stronger here; A is more specific in that it guarantees more in its postcondition

int find2( int[] a, int value ) {
  for ( int i = a.length - 1 ; i >= 0 ; i-- ) {
    if ( a[i] == value ) return i;
  }
  return -1;
}

  • The find2() method satisfies only Spec B (and NOT Spec A)

int find( int[] a, int value ) {
  for ( int i = 0 ; i < a.length ; i++ ) { if ( a[i] == value ) return i; }
  return -1;
}

Specification A:
requires: a is non-null and value occurs in a
returns: index i such that a[i]=value

Specification B:
requires: a is non-null
returns: index i such that a[i]=value or index i=-1 if value is not in a

  • Does find() satisfy both of these specifications? Yes.
  • Which specification is stronger? Spec B is stronger
  • If implementation I satisfies Spec B, then that implies that it also satisfies Spec A
  • Note that the reverse is not true! Spec A does not imply Spec B (e.g., for Spec A, an implementation might return 999 if value is not in the array a)

String substring( int beginIndex )

Specification A:
requires: 0 <= beginIndex <= length of this String object
returns: new String with same value as the substring beginning at beginIndex and extending until the end of the current String

Specification B:
requires: nothing
returns: new String with same value as the substring beginning at beginIndex and extending until the end of the current String
throws: IndexOutOfBoundsException — if beginIndex is negative or greater than the length of this String object

  • Which one is stronger? Spec A or Spec B? (answer far below…..)

Answer: Specification B is stronger. Specification A is weaker because it requires more and guarantees less.