It is sometimes helpful to include in a program various variables or computations that are only for specification. For example, a ghost field might keep track of information about a class that the Java implementation does not. Or, in the body of a method, one may want to record some value or perform some computation for the purpose of checking the Java implementation, but not have that variable or computation be part of the Java implementation or compiled into the runnable class.
ghost declarations and various JML-only statements for this purpose.
- Field declarations can be modified with the
ghostkeyword and placed in a JML comment. Such fields are in scope for specifications but not in Java code.
- Model field methods and classes are also specification-only constructs.
- The JML
setstatement permits assignments and computations:
//@ ghost int i = x; // x may be a Java variable //@ set i = i + 10; // a ghost computation
setstatements may also include pure method calls.
The values of
ghost variables may then be used in subsequent JML
assert statements, for example.