# 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:

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

Basic exercises – basic invariants exercises

Preserved blocks – teaches you how to use preserved blocks and

`requireInvariant`

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

Ghost exercises – contains several exercises for ghosts and invariants