Specification variable semantically behaves like program variable, but has the property that it can be removed when the program executes, without affecting program execution.

The purpose of program variable is to describe program properties.

It is therefore similar to expressive types: such types are also removed at run-time:

• parametric types are removed in compilation of Scala and Java 1.5, because JVM does not support them
• most type information is removed when compiling to machine code, for example, no information about different classes is preserved

Because we can write invariants that connect specification variables and concrete variables, we can use specification variables to describe properties that are more expressive than properties of typical type systems.

Among uses of specification variables are:

• indicating when global invariants should hold
• specifying public interface of methods that do not reveal concrete implementation of a class/module
• proving that the observable behavior of one module is included in observable behavior of another module
• using first-order logic to specify invariants that would otherwise require more expressive logic over program states (such as transitive closure or inductively defined properties)
• supplying witnesses for existentially quantified statements
• combining multiple reasoning procedures

There are two kinds of specification variables:

• those that need to be explicitly updated, like ordinary variables (and usually have invariants that constraint their possible values)
• those that come with a defining expression and whose value is automatically computed at certain points of the program

More information:

• Modular Data Structure Verification
• Full Functional Verification of Linked Data Structures
• An Integrated Proof Language for Imperative Programs