Ghost variables can be

• assigned (arbitrary values, possibly depending on other specification varibles)
• havoc-ed
• 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);

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

References:

• Principles of Computer Systems in MIT OpenCourseware
  • Problem 3
  • Solution 3
• 2007 Model Checking Course at EPFL