Elimination of Ghost Variables in Program Logics
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
- PDF / 270,846 Bytes
- 20 Pages / 430 x 660 pts Page_size
- 67 Downloads / 220 Views
Institut f¨ ur Informatik LMU M¨ unchen, Germany 2 Trusted Labs, Sophia-Antipolis, France [email protected], [email protected]
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.
1
Introduction
With the fast development of programming systems, the requirements for software quality also become more complex. In reply to this, the techniques for program verification also evolve. This is the case also for modern specification languages which must support a variety of features in order to be expressive enough to deal with such complex program properties. A typical example is JML (short for Java Modeling Language), a design by contract specification language tailored to Java programs. JML has proved its utility in several industrial case studies [1,2]. Other examples are ESC/Java [3], the Larch methodology [4] and Spec# [5]. JML syntax is very close to the syntax of Java. JML has also other specification constructs which do not have a counterpart in the Java language. While program logics and specification languages help in the development of correct code they have also been proposed as a vehicle for proof-carrying code [6,7,8,9] where clients are willing to run code supplied by untrusted and possibly malicious code producers provided the code comes equipped with a certificate in the form of a logical proof that certain security policies are respected. In this case, the underlying logical formalism must have a very solid semantic basis so as to prevent inadvertent or malicious exploitation. On the one hand, the logic must be shown sound with respect to some well-defined semantics; on the other hand, the meaning of specifications must be as clear as possible so as to minimise the risk of formally correct proofs which nevertheless establish not quite the intuitively intended property. This calls for a rigorous assessment of all the features employed in a specification language; in this paper we do this for JML’s ghost variables. G. Barthe and C. Fournet (Eds.): TGC 2007, LNCS 4912, pp. 1–20, 2008. c Springer-Verlag Berlin Heidelberg 2008
2
M. Hofmann and M. Pavlova
Coq development. All definitions, theorems, proofs have been carried out within the Coq theorem prover and are available for download at www.tcs.ifi.lmu.de/ ~mhofmann/ghostcoq.tgz.
2
Ghost Variables and Their Use
In brief, a ghost variable is an assignable variable that does not appear in the executable code but only in assertions and specifications. Accordingly, annotated code is allowed to contain ghost state
Data Loading...
