SC specifications

software engineering › 6.031 software construction

R6: specifications

Behavioral equivalence

whether it could be substituted with one implementation for the other

1
2
3
4
static int find(...){
	//requires: ........
	//effects:
}

Specifications

why

  • Acts as firewall
  • Connect / separate client and implementer
    • Client: input, output
    • Implementater: computation
      • Local variables, private fields, implementation details

structure

  • Composition
    • method signature
    • requires clause -> additional restrictions on the parameters
      • type
      • interactions between parameters
    • effects clause -> return value, exceptions, and other effects of the method
      • How the return value relates to the inputs
      • exceptions
      • Whether and how objects are mutated
  • precondition and postcondition of the method
  • Overall structure:
    • if the precondition holds, then the postcondition must hold when the method completes
    • Else, free to do anything

in java

  • javadoc
1
2
3
4
@param p
@param q
@return
@throw

do not allow null references

  • syntactically illigal
    • primitives cannot be null
    • Some methods or fields: length()
  • Null values are vague
    • Disallowed in parameter and return values unless spec says otherwise
    • use something other than null makes your meaning clear
    • Fail fast: null can overlook many kinds of bugs
1
2
Map.get(key) return when the key is not found in the map: 
Optional<T>

Include emptiness

  • difference between null and emptiness

  • empty values are alway allowed as parameter or return values.

~ testing

  • Black box tests need follow specification
  • Glass box test must follow spec too.

~ mutating

  • describe side-effects-changes to mutable objects-in the postcondition
  • Mutation is disallowed unless stated otherwise

exceptions

  • Function
    • Signaling bugs
    • for special results
  • checked and unchecked exceptions
  • exception hierarchy
  • declare exceptions in specs

R7: design specifications

Three dimensions for comparing specs

  • deterministic
  • declarative
  • strong

Deterministic vs. underdetermined specs

  • deterministic: one final state for the same input.
  • undetermined: multiple valid outputs for the same input
    • different from Nondeterministic, which means same program with the same inputs can generate different outcomes

Declarative vs. operational specs

  • Operational : steps that the method performs
  • Delcarative : properties of the final outcome, and how it related to the initial state

stronger vs. weaker specs

a spec S2 is stronger than a spec S1 if the set of implementations that satisfy S2 is a strict subset of those that match S1.

Rule: S2 is stronger than a spec S1 iff

  • S2’s precondition is weaker than or equal to S1.
    • S2’s input is less, placing fewer demands on a client
  • S2’s postcondition is stronger than or equal to S1.
    • Make more promises to the client