Elimination of Ghost Variables in Program Logics

Abstract. Ghost variables are assignable variables that appear in program annotations but do not correspond to physical entities. They are used to facilitate specification and verification, e.g., by using a ghost variable to count the number of iterations of a loop, and also to express extra-functional behaviours. In this paper we give a formal model of ghost variables and show how they can be eliminated from specifications and proofs in a compositional and automatic way. Thus, with the results of this paper ghost variables can be seen as a specification pattern rather than a primitive notion.

• Type: Conference
• Year: 2007
• Where: TGC
• Authors: Martin Hofmann, Mariela Pavlova
• Keywords: Applied Computing, Assignable Variables, Ghost Variables, Paper Ghost Variables, TGC 2007