Elimination of Ghost Variables in Program Logics

9 years 2 months ago
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.
Martin Hofmann, Mariela Pavlova
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TGC
Authors Martin Hofmann, Mariela Pavlova
Comments (0)