key observations about specifications
specifications must be explicit
independent development and testing
resources are finite
program specs evolve over time
testing
a form of consistency checking between implementation and spec
black box testing
you see nothing about the program’s internal mechanisms
white box testing
all program internal details are available
grey box
between white and black box testing
automated vs manual
automated:
- find bugs more quickly
- no need to write tests
- if software changes, no need to maintain tests
manual
- efficient
- sometimes better coverage
black box vs white
black
- can work with code that cannot be modified
- does not need to analyze or study code
- can be performed in any format
white
- efficient test suite
- better coverage
classification of specs
safety properties:
- program will never reach a bad state
- e.g. assertions, types, type-state properties
liveness properties:
- program will eventually reach a good state
- e.g. program terminations, starvation freedom
common forms of safety properties
types: int x, java.net.Socket s, …
type-state properties: program must not read data from java.net.Socket until socket is connected
assertions: implicit, e.g. p != null before each dereference of p
pre and post conditions: double sqrt(double x) {…}
pre-condition: x >= 0
post-condition: return value ‘ret’ satisfies ret * ret = x
types
adding the specification to the implementation allows to check the implementation against the specification
checker framework
goal: statically eliminate entire classes of runtime errors via annotations
two kinds of useful invariant
loop invariant:
- a property of a loop that holds before and after each iteration
- captures the essence of the loop’s correctness, and by extension of algorithms that employ loops
class invariants:
- a property that holds for all objects of a class
- established upon the construction of the object and constantly maintained between calls to public methods
houdini algorithm
