4. Invariants and Ghosts

This lesson walks you through using invariants in CVL specs, and using ghost variables with invariants. An excellent exposition of invariants is given in the Invariants Documentation, and the sections Writing an invariant as a rule and Invariants and induction are particularly illuminating. For introduction to invariants read the Invariants Overview section.

The second half of this lesson deals with ghost variables. Ghost variables are additional variables defined in the spec. We can use them to keep track of various actions occurring in the code. There is a basic introduction to ghost variables in the Ghosts Documentation.

Contents:

1. Simple invariants examples – simple invariant examples, including the illuminating Ball Game example

2. Basic exercises – basic invariants exercises

3. Preserved blocks – teaches you how to use preserved blocks and requireInvariant statements

4. Ghosts and hooks – the basics of using ghosts with hooks, focusing on their use in invariants

5. Ghost exercises – contains several exercises for ghosts and invariants