A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. This may be code that expresses the very properties you want to prove, or code that allows naming in properties some quantities that would have no name otherwise. This is more common when proving richer properties (for example an integrity, functional or security property), but this may also be needed when proving a "mundane" property like absence of run-time errors.

If you're careful or lucky enough, the additional code you write will

1. not impact the program being verified, and
2. be removed during compilation, so that it does not inflate binary size or waste execution cycles.

But SPARK provides a better way, by marking the corresponding code as ghost code, using the new Ghost aspect. This instructs GNATprove to check property 1 above and GNAT to ensure property 2 above. For example, a function that is only used in contracts and assertion pragmas can be marked as ghost as follows:

and a variable that is only used to store or compute values read in contracts and assertion pragmas can be marked as ghost as follows:

Besides declarations of ghost entities (packages, subprograms, types or variables), ghost code consists also of:

• statements that assign to a ghost variable
• calls to ghost procedures
• contracts and assertion pragmas that refer to a ghost entity

The identification of ghost code in SPARK is thus mostly syntactic, which ensures both that ghost code is visibly ghost to programmers and easily removed by GNAT during compilation. At the same time, SPARK has verification rules that ensure that ghost code cannot impact the functional behavior of non-ghost code, and that users cannot partly disable updates to a ghost variable (either all updates must be enabled, or they must be disabled). GNATprove checks those rules.

On the one hand, ghost code in SPARK is mostly targeted at facilitating proofs, a direct descendant from auxiliary variables used in the 60s (see the Related Work section of the article The Spirit of Ghost Code). On the other hand, ghost code in Ada or SPARK provides a strong mechanism for safe code instrumentation, reminiscent of aspect programming principles.

For more examples of uses of ghost code, see the section of SPARK User's Guide on Ghost Code.

For an advanced use of ghost code to perform manual proof, see this previous post.