Soundness of Simple Ghost Variables
Ghost variables can be
- assigned (arbitrary values, possibly depending on other specification varibles)
- used in assert statements, preconditions, postconditions, invariants
We call the part of the state given by program variables the abstract state.
We are not allowed to do use ghost variables to affect the concrete state, in particular:
- no assigning ghost to non-ghost variables
- no use of ghost variables in if and while conditions
The correctness condition on specification variables:
If the program with ghost variables succeeds, then the program without specification variables also succeeds (does not fail assertion) and produces the same result.
When is it acceptable to allow users to write
havoc x,y suchThat F(x,y)
if x,y are ghost variables?
How can we translate this construct into simple statements (havoc,assume,assert)?
Example: given a program containing variable x, is it safe to add a specification variable y together with the condition
havoc(y); assume(y * y = x);
Correctness Using Forward Simulation Relations
Labelled transition system
Notion of observable program trace
- recording procedure calls of a module together with parameters and results
- example: implementation of a container data structure with 'insert' and 'member' functions
- specifications as missing aspect of object-oriented programming
Trace inclusion and proving it by induction
Forward simulation relation
Backward simulation relation