The logic of ESC/Java

ESCJ 8a. By Rustan and Jim, 30 December 1997. Some additions by Cormac 24 April 1998. Modified by Rustan, 13 September 1999 (making ESCJ 8a from ESCJ 8).

This document describes the logic of ESC/Java.  It describes axioms that are part of the logic (and thus are always included in the background predicate) and axioms that are introduced to the background predicate when the Java program being checked contains various constructs.  It is not the purpose of this document to describe the translation of Java into guarded commands, but we describe some of the assumptions and assertions produced by the translation when this will help the reader understand the interaction between the translation and the logic.

When we introduce constants, predicates, and functions, we display an indented pseudo-declaration, which includes a signature.  These signatures are just for our intuitive understanding, since the logic is untyped.  Appendix A, List of predicates, functions, and constants, summarizes all such pseudo-declarations in this document.  We display axioms as solid-bulleted items; the mere appearance of the pseudo-declaration of an operator does not implicitly give rise to any axiom.  In the discussion of axioms, we will use hollow bullets to indicate possible alternative axioms or axioms that might be generated in illustrative examples.  We will use square bullets to display expressions that are produced as part of assumptions and assertions by the translation.  (We wish HTML supported hollow square bullets as well.)

In this document, small print discusses open design issues.

This document was written under the heavy influence of Dave Detlefs's Logic of ESC/Modula-3.

0  Preliminaries

The ESC/Java tool attempts to find errors in Java programs by translating annotated Java programs into guarded commands, deriving weakest preconditions for those guarded commands, and testing those preconditions with a theorem prover.  We have chosen to use Simplify as that theorem prover.  Our design of the logic of ESC/Java is strongly influenced both by the underlying logic of Simplify (of which our logic is an extension) and by efficiency considerations specific to Simplify.  In this section, we describe, more or less, what the reader needs to know about Simplify in order to understand the logic and the motivation for some of our design decisions.

0.0  Terms and predicates

Simplify's logic is untyped, but makes a strong distinction between terms and predicates.  Terms are expressions that represent values in an underlying value space.  Predicates are expressions that represent truth values.

A term in Simplify is a term constant, a variable, or an application of a function to terms.  Simplify provides some built-in term constants, such as 0 and 6, and some built-in functions, such as +.  It also provides mechanisms by which users can implicitly declare constants, variables, and functions.

A predicate in Simplify is predicate constant (like TRUE), an application of a built-in predicate symbol to terms, an application of a boolean connective to predicates, or a quantified predicate.  Simplify's built-in predicate symbols include ==, !=, and <; its built-in boolean connectives include &&, ||, and !.  (The actual symbols used by Simplify differ from those in this document, which uses a Java-like syntax.  For example, we write x != y where Simplify expects (NEQ x y).  The different syntax should not create any confusion, except possibly for the built-in predicate symbol EQ and the built-in boolean connective IFF, both of which we write as ==.  We hope the context of == will help disambiguate.)  Throughout this document, the implication operator ==> binds more loosely than other logical connectives.

While Simplify does not allow a user to declare new predicate symbols, it allows the user to designate some function symbols to be usable where predicate symbols are expected.  If f is such a function symbol, then whenever Simplify encounters an expression f(...) where a predicate is expected, it treats this expression, which would normally represent a term, as sugar for the predicate f(...) == boolTrue.  (Note that boolTrue is a built-in term constant, not the built-in predicate constant TRUE.)  We refer to such a function symbol f as a user-defined predicate symbol or, by even greater abuse of the language, a predicate.  In this document, we write

to show that we intend to use the function symbol as a user-defined predicate symbol.

0.1  Quantifiers and triggering patterns

We said above that Simplify has term constants and variables, but we weren't specific about what distinguishes them.  Constants include not only numeric literals such as 6, but also symbolic constants that the uninitiated reader might naïvely perceive as variables.  Symbol names are considered variables only when they are bound by a quantifier.  As an example, consider the following axioms for group theory: Here, x, y, and z are variables, but e is a constant.  As another example, if Simplify is given the axioms (from which it could successfully prove the conjecture s + f(s) < 2 * t), then s and t are constants whose values are not known, other than that they satisfy the given axioms.  The axiom s < f(s), in which s is a constant, is entirely different from in which s is a variable.

A ground term is a term that contains no variables.  The heart of Simplify's proving machinery is a set of procedures for testing the satisfiability of collections of equalities, distinctions (!=), and arithemetic inequalities of ground terms.  To handle the boolean connectives, Simplify uses case analysis; to handle quantified expressions, Simplify uses Skolemization and matching as explained next.

When a quantified predicate is postulated to have a definite truth value--either directly by the user or as a result of case analysis--one of two things happens.  If an existentially quantified predicate is postulated to be TRUE, Simplify introduces a Skolem constant for each of its variables, substitutes the Skolem constants for the variables in the body, and postulates the result.  If a universally quantified predicate is postulated to be TRUE, Simplify produces a matching rule.

A matching rule represents a universally quantified predicate in a form that enables the prover to produce potentially relevant instantiations of its body in response to the detection of ground terms matching certain triggering patterns.  For example, postulating the axiom

produces a matching rule with the triggering pattern times(e, x).  Whenever the prover finds a ground term of the form times(e, T), it will instantiate the body of the axiom with x := T, that is, it will postulate times(e, T) == T.

The choice of triggering patterns for matching rules can impact both the completeness and the performance of the prover.  Simplify has heuristics for automatically choosing triggering patterns, but allows a user to override the heuristics and specify the triggering patterns explicitly.  In this document, we use underlining to indicate the triggering patterns of matching rules.  For example, we would write the group theory identity axiom as

to indicate that times(e, x) is used as the triggering pattern of the resulting matching rule.  In order to improve performance, we have attempted to write axioms and choose triggers in such a way as to reduce the cost of pattern matching and to reduce the likelihood that the prover will produce instantiations that lead to useless case splits.  It might be tempting, in the quest for efficiency, to write axioms that are actually inconsistent and to depend on the choice of restrictive triggers to prevent the inconsistency from coming into play and causing bogus verifications to succeed; we have resisted this temptation.

Sometimes we must use a set of terms as a triggering pattern instead of a single term.  For example, for a quantified predicate like

no single term is an adequate trigger, since no single term contains all the quantified variables.  An appropriate trigger is the set of terms {member(x, s), subset(s, t)}: With this multi-trigger, the body will be instantiated upon the detection of a pair of ground terms matching member(x, s) and subset(s, t), with the same ground term matched to s.  Although sometimes needed, multi-trigger matching is generally more expensive than single-trigger matching.

Note that triggering patterns are sets of terms, not predicates.  Thus, it is not possible to specify the following trigger:

Neither is it possible to specify a trigger containing a built-in predicate symbol, such as < or ==.

0.2  Predicate definitions

Simplify provides a mechanism by which a defining expression may be provided as part of the declaration of a user-defined predicate symbol P.  Whenever an application of P is made equal to or distinct from boolTrue, the defining expression is instantiated with appropriate substitutions for the arguments and the resulting predicate or its negation, respectively, is postulated.  By using this kind of definition, instead of separately introducing a universally quantified axiom, two sorts of efficiency improvements may result.  First, we avoid invoking Simplify's general purpose pattern matching.  Second, by instantiating the definition of a user-defined predicate only when an application's truth value becomes known, rather than when an application is introduced, we may avoid gratuitous case splitting.  (Of course, there is a danger that we will sometimes postpone useful case splitting.)

When in this document we intend a given axiom (ALL args :: P(args) == ...) to be the defining expression for a user-defined predicate P, we will use the notation

0.3  The as trick

In this section, we describe a technique, used in several of the axioms below, that allows us to choose triggering patterns that Simplify can match efficiently but that will not lead to extraneous matches.

In a world with types, a typical axiom might look like

where x is quantified over all values of type X and y is unconstrained.  Since Simplify is type-free, so is our logic.  The straightforward way of encoding the axiom above would be to introduce a predicate isX characterizing values of type X: But what should be the triggering pattern of this axiom?

If we choose P(x, y) as the triggering pattern, then Simplify is likely to instantiate the axiom with substitutions x, y := t0, t1 even where t0 is not known to satisfy isX.  The result may be to cause the prover to do a useless case split with the cases ! isX(t0), ! P(t0, t1), and Q(t0, t1).  Even if P(t0, t1) is known to hold, we can get a two-way case split.

Intuitively, we want to use the axiom only when x is already known to be of the correct type--this would be the common interpretation of the typed version of the axiom.  If we can arrange for other mechanisms to postulate isX(x) whenever we're possibly interested in instantiating the axiom, then we can use the terms isX(x) and P(x, y) together as a multi-trigger.  This reduces the likelihood of producing useless instantiations of the axiom, without loss of completeness.  If, further, we make sure that ground terms matching isX(x) are introduced only when they are also equated to boolTrue, then the untyped axiom will be instantiated only as often as the typed version would have been in a typed prover.

A disadvantage of the approach just described is that Simplify's matching process for multi-triggers is generally more expensive than for ordinary triggering patterns.

Instead of introducing the predicate isX, the approach we actually take is to introduce a function asX.  Intuitively, asX casts any value into a value of type X, and is the identity on values that are already of type X.  When introducing a term t0 of type X, instead of assuming

we assume This allows us to write the axiom as Here we have a single-term trigger, which should be efficient to match.  Also, since we introduce asX only with arguments that are known to be of type X, we avoid producing irrelevant instantiations.

(We could introduce both isX and asX, in which case we could either define isX(x) by the axiom

or characterize asX by the axioms However, once we have asX, introducing isX seems redundant.)

In the example above, we replaced a one-argument predicate isX with a one-argument function asX.  We can apply a similar technique for predicates with more than one argument.  For example, instead of writing an axiom of the form

we may introduce a function asXwrtZ, assume x == asXwrtZ(x, z) when we would have assumed isXwrtZ(x, z), and write the axiom as Multi-argument predicates like isXwrtZ are used to express more intricate properties than types can.

0.4  Maps

ESC/Java uses maps to represent instance variables, arrays, and lock sets.  A map is like a function, but is a first-order value in the logic.  The logic includes the following functions on maps: The [ ] function is sometimes called select.  The semantics of [ ] and store are given by the following axioms: ESC/Java uses Simplify's built-in select and store functions.  The second of these axioms is treated specially by Simplify in that the case splits suggested by it are given some priority over case splits suggested by ordinary axioms.

1  Types and subtypes

1.0  Types

Java types are ordinary values in the logic of ESC/Java.  Although the logic is untyped, we informally think of these values as having type "type".

The built-in types in Java give rise to the following type constants:

In addition, declarations of classes and interfaces give rise to type constants.  Each class or interface declaration

     class T ...

or

     interface T ...

introduces a type identifier

Here and throughout this document, we assume that identifiers denoting types, fields, and variables have been unique-ified.  Throughout this document, when we refer to declarations, we include both user-provided declarations and built-in declarations, like the classes String and Object, the interface Cloneable.

All type constants appear together in an axiom that postulates them all to be different:

This axiom is called the Distinct Types Axiom.

1.1  The subtype predicate

The logic includes a subtype predicate: The predicate t0 <: t1 means that t0 is a subtype of t1.  The operator <: binds as tightly as arithmetic relations such as <.

The following axioms are sound and complete in the sense that for any named class or interface types A and B,
 
     |= A <: B    if and only if    |- A <: B

where |- refers to provability based on these axioms, and |= refers to the model given by Java's semantics.
In some cases we also need to prove negative subtype statements such as

     |- not( A <: B )

To illustrate the need for proving such statements, see Appendix B example 3. Our current axiomatization of negative subtype statements is quite incomplete -- we currently only include the antisymmetric axiom. We plan to investigate this issue more thoroughly in the future.

The subtype relation is reflexive and transitive:

The subtype relation is also antisymmetric. An alternative would be to experiment with Simplify's built-in ordering theory, but we have concerns about its reliability and its impact on performance.

A class or interface declaration gives rise to axioms about where the type introduced fits into the subtype ordering.

For each class declaration

    class C extends D implements J, K, ...

(where the absence of an extends clause is taken as sugar for extends Object), we add the following axioms to the background predicate:

We could include an axiom that describes the supertypes of C   For the built-in class Object, this would yield For each interface declaration

    interface I extends J, K, ...

we add the following axioms:

We could include an axiom describing the supertypes of I, as above, but see no immediate need for it.

For each final type T (that is, a final class or one of the primitive types boolean, char, byte, short, int, long, float, or double), we add the following axiom, which says that T has no proper subtypes:

To see why this axiom is useful, see Appendix B example 1.

1.2  Disjointness of incomparable classes

This section is not implemented. It may be useful for examples such as Appendix B example 3.

The axioms in this section are similar to some axioms introduced in the logic of ESC/Modula-3 to address a problem that arose in a program verification.  It is not clear whether the problem has since been addressed by other mechanisms.  While we can contrive examples where these axioms would be necessary for ESC/Java verifications, we don't know if such examples will arise naturally.  We may choose not to exclude the material in this section without impact on the rest of the logic.  In particular, there are no uses the functions classDown and asChild other than those described in this section.

For any two classes, either one is a subtype of the other, or they have no subtypes in common.  The most obvious ways of axiomatizing this fact seem likely to lead to poor prover performance, for reasons that we will not describe further.  The ESC/Java logic includes weaker axioms implying that distinct explicitly declared subclasses of any class (including Object) have no subtypes in common.

To this end, the logic includes two functions:

Intuitively, if t0 is a proper subclass of t2, then classDown(t2, t0) is the direct subclass of t2 that is a superclass of t0.  Consider a class A with distinct explicitly declared direct subclasses B and C, and suppose that BB is any subclass of B and CC is any subclass of C.  Then, classDown(A, BB) is B and classDown(A, CC) is C.  If Simplify ever explores a case in which BB and CC are equal, it will infer by congruence closure that classDown(A, BB) and classDown(A, CC) are equal, and thus that B and C are equal, in contradiction to the Distinct Types Axiom in Section 1.0.  Of course, if BB and CC were explicitly declared classes, we could infer their distinction directly from the Distinct Types Axiom.  However, BB and CC might be the unknown dynamic types of objects with declared types B and C, respectively.

We want to formalize the definition of classDown.  To do so, we must first formalize the notion of being a direct subclass.  We could introduce a predicate isDirectSubclass, characterize classDown by the axiom

and let each class declaration

    class C extends D ...

give rise to the axiom

Instead, we avoid use of a multi-trigger by employing the as trick (Section 0.1):  We characterize classDown by the axiom and for each class declaration

    class C extends D ...

we introduce the axiom

1.3  Array types

Array types do not give rise to type constants.  Instead, the logic includes a function to produce an array type from an element type. If t represents a type T, then array(t) represents the array type T[].

Sometimes in this document we make reference to an arbitrary type T, which may or may not be an array type.  For simplicity, we will denote its type T, even though the type of T may in fact not be represented by a type constant, but by an expression array(...).

All array types are subtypes of Cloneable:

Note that since Cloneable is a subtype of Object, every array type is, by transitivity, also a subtype of Object.   Conversely, Object and Cloneable are the only non-array supertypes of array types, so for each class declaration

    class T ...

(except for the built-in class Object) or interface declaration

    interface T ...

(except for the built-in interface Cloneable), we could add the axiom

An alternative approach would be to generate the axiom (ALL t0, t1 :: array(t0) <: t1 ==> t1 == array(elemType(t1)) || Cloneable <: t1), where elemType is defined below.  Technically, this is more complete, but it seems more likely to lead to unfruitful case splits.

The function array has a left inverse:

Intuitively, a type t is an array type if and only if t == array(elemType(t)).  We could introduce a predicate isArrayType with the axiom Instead, we simply write t == array(elemType(t)) wherever we would have written isArrayType(t).

While Object and Cloneable are not array types, they are supertypes of all array types.  The non-object primitive types boolean, char, etc. are not supertypes of any array types, but we have not given axioms to that effect, because we are not sure they are needed in practice.  The axioms we just gave, however, may be useful, as Motivating Example 0 show.

 
As stated in the following axiom, the subtypes of an array type T[] are the array types whose element types are subtypes of T. A use of this axiom is described in Appendix B example 1 and 2.

2  Types of values

2.0  The is predicate

To reason about the dynamic types of values, the logic includes the following predicate: For each variable identifier (global variable, parameter, or result value) v of type T, we assume as part of the precondition of the method being checked, after each method call that modifies v, and as an invariant of each loop that modifies v.

2.1  Casting

The logic contains a function that converts a value to a value of a specified type: If the value is already of the specified type, then casting leaves it unchanged: In cases where casting in Java can fail, the translation produces appropriate checks.  These checks will be described in another document.

The axioms above do not completely capture the semantics of casting as specified by Java.  For example, Java specifies that casting an int to a short preserves the value modulo 2^16.  We propose to omit such additional axioms about casting until the need for them arises.

2.2  Types of primitive values

2.2.0  Booleans

For booleans, the logic contains two distinct constants: In fact, these are the only boolean values.  We could express this fact with the axiom Since this axiom has the potential to lead to useless case splits, we're reluctant to use it.  In Section 5.2, Reflections of predicates into term space, we'll say more about our approach to handling booleans.

2.2.1  Integers

To reason about the ranges of integer values, the logic includes the constants: and the following axioms: The reason for giving longFirst, intFirst, intLast, and longLast as symbolic constants instead of exact values is that we don't want to assume the underlying theorem prover to be capable of dealing properly with such large constants.
Will the use of constants like 65535 and 127 cause performance problems because of Simplify's integer programming heuristic? Complications arise when the Java program being checked contains explicit integer constants of large magnitude.  Our plan for treating such constants is to replace all explicit constants whose magnitude exceeds some threshold (say, 1000000) with symbolic constants, and to add to the background predicate sufficient axioms to establish the ordering of those symbolic constants with respect to each other, the threshold and its negation, and the symbolic constants longFirst, intFirst, intLast, and longLast.  For example, if the program contains the explicit constants then, using 1000000 as a threshold, the constants -12000000, 12000000, 123456789, and 1234567890123456789L will be replaced by the symbolic constants neg12000000, pos12000000, pos123456789, and pos1234567890123456789, and the following axioms will be added to the background predicate: Note that in the absence of such large constants, we will have the following axioms: The axioms we have described for casts and integer values are sufficient to guarantee, for example, that casting a short to an int does not change its value.  Also, when an int is in the range -32768..32767, casting it to a short does not change its value.  For an int that is not already a short,  the axioms guarantee that casting it to a short will yield a result in the range -32768..32767, but don't specify the exact result even though the Java specification does.
It remains to be seen if practice calls for more axioms.

2.2.2  Floating point values

The ESC/Java logic is weak in its treatment of floating point values. The following are not implemented. Note that, despite these properties, int and float are not subtypes of double.  (If they were, array(int) and array(float) would be subtypes of array(double), according to the axioms about array in Section 1.3.)

2.3  Types of objects

Every non-null object has a unique dynamic type, as determined by the typeof operator: A value is of a reference type T if the value is null or if its dynamic type is a subtype of T: We said in Section 2.0 that the translation will introduce a precondition assumption is(v, T) for any parameter v of type T.  For the this parameter of an instance method of a class C, the translation introduces the following stronger precondition:

2.4  Instantiable types

The dynamic type of a non-null object must be an instantiable type.  The logic could includes a predicate and the axiom For each interface declaration

    interface T ...

or abstract class declaration

    abstract class T ...

the background predicate contains the following axiom:

Is instantiable useful in practice?  We can omit the predicate instantiable and its associated axioms without impact on the remainder of the logic.

2.4  Types of instance variables

ESC/Java models instance variables (fields) as maps from objects to values.  Where in Java one writes the r-value x.f, the translation writes f[x].

To reason about the dynamic types of values of fields, the logic includes the following function:

To encode that a field identifier f has range type T, the translation introduces the assumption as part of the precondition of the method being checked, after each method call that modifies f, and as an invariant of each loop that modifies f.  This is another application of the aforementioned as trick.  The logic includes the axiom Notice that this axiom does not include an antecedent requiring that x be a non-null object of the class that declares f.  We believe that this treatment of a fields as total maps with their declared range types is harmless to the soundness of the logic, and may be beneficial to prover efficiency.

2.5  Types of array elements

ESC/Java models the state of all arrays using a single global variable called elems.  Where in Java one writes the r-value a[i], the translation writes elems[a][i].  This uses the same select function as above for fields, twice.
An alternative to using a single global variable elems would be to use a variable objectElems to model all arrays of objects and additional variables for each of the primitive types, with intElems modeling all arrays of ints, etc.  Having separate variables may improve prover efficiency, but would complicate the translation into guarded commands (and the logic itself).  We propose to keep things simple for the initial version of ESC/Java.

To reason about the dynamic types of array elements, the logic includes the following function:

Applying yet again the as trick, the translation introduces the assumption as part of the precondition of the method being checked, after each method call that modifies elems, and as an invariant of each loop that modifies elems.  This assumption is used to supply a trigger for the following axiom: Notice that this axiom does not include antecedents requiring that a be a non-null array object and that i be in bounds.  We believe that this treatment is harmless to the soundness of the logic, and may be beneficial to prover efficiency.

3  Allocation

In this section, we introduce machinery for reasoning about the allocation of objects, and in particular for showing that a newly allocated object is distinct from any object reachable from program variables prior to its allocation.  Although our motivating discussions are long, the resulting axioms are few and simple.

3.0  Allocation times of objects

Consider the following method:

    void m(T x) {
      T y = new T();
      /*@ assert x != y; */
    }

Intuitively, the reason that the assertion succeeds is that x is already allocated at the start of the method body, whereas the result of the constructor call new T() is an object not yet allocated before the call.  To formalize this, we introduce a program variable alloc, which somehow models which objects have been allocated.  As we shall see below, we actually model alloc as a time.  We also introduce a predicate

where isAllocated(x, aa) means that object x has been allocated prior to time aa.  For each variable identifier (global variable, parameter, or result value) v of an object type, the translation assumes as part of the precondition of the method being checked, after each method call that modifies v, and as an invariant of every loop that modifies v.  Finally, the translation includes the following postcondition as part of the specification of new T(): where alloc and alloc' are the values of alloc before and after the call, respectively, and result is the value returned by the call.  The guarded command translation of the method m is thus something like: The verification condition for this piece of code is: so the verification succeeds.

Now, consider the following method:

    void n(T x) {
      p();
      T y = new T();
      /*@ assert x != y; */
    }

where p() denotes a method call that modifies alloc.  In order to verify the assertion, we must be able to infer that x is still allocated after the call to p.  One possible approach would be for the translation to explicitly assume

after the call [oh, how we wish we had hollow square bullets...].  We reject this approach, since it would require generating such an assumption for each variable in the program, instead of just those that are modified by the call.  Another approach would be for the translation add to the following as a postcondition of every method that modifies alloc: We actually use yet a different approach, which we hope will achieve better efficiency by making use of Simplify's built-in Simplex algorithm.  First, we let alloc denote a time.  Second, we introduce a function from objects to their allocation times: Third, we define isAllocated in terms of vAllocTime and Simplify's built-in < operator: Fourth and finally, the translation assumes after every method call that modifies alloc (where alloc0 is the value of alloc before the call), and as an invariant of every loop that modifies alloc (where alloc0 is the value of alloc before the loop).
Is it worth attempting to detect cases where method calls leave alloc unchanged as far as the caller is concerned?

3.1  Closure of allocatedness under field access

In Section 3.0, we introduced rules by which ESC/Java can verify that a newly allocated object is distinct from previous values of program variables.  We may also need to verify that newly allocated objects are distinct from all objects accessible prior to allocation, as in the following example:

    void m(U u) {
      T y = new T();
      /*@ assert u.f != y; */
    }

Indeed, it is an invariant of the language that fields of allocated objects are allocated.  In this subsection, we show how ESC/Java formalizes this invariant.

One possible way to formalize the invariant would be to introduce a predicate isFieldClosed, characterized by the following axiom:

and to have the translation to assume, at appropriate points, isFieldClosed(f, alloc) for each field f whose range type is an object type.

The question now is:  What are "appropriate points"?  It would be nice not to have to re-assume isFieldClosed(f, alloc) after calls to a method m that does not modify f, even if m modifies alloc.  Consider an object x such that isAllocated(x, alloc) holds after some call to m, and suppose we need to infer that isAllocated(f[x], alloc) holds.  We proceed by case analysis:  If isAllocated(x, alloc0) holds, where alloc0 is the allocation time before the call to m, then by the axiom above isAllocated(f[x], alloc0) holds.  From m's postcondition alloc0 <= alloc, the definition of isAllocated, and the transitivity of <, the desired inference is possible.  Suppose, on the other hand, that ! isAllocated(x, alloc0).  Then, f[x] == null, since f was not changed.  Hence, we're done.

There are two problems with the approach just described.  First, it may give rise to unnecessary case splits.  Second, it inhibits an optimization that we'd like to do:  If a method m modifies a field f only at newly allocated objects, we don't want to require that f be included in the modifies clause of m's specification.  Thus, we cannot assume, as we did in the informal proof above, that f is null at unallocated objects.  Instead, the model we use is that, as seen by the caller, the method m allocates objects whose f fields already have the "right" values.  Indeed, m might be seen as allocating a "pre-existing" cyclic structure of objects.  Hence, what we would like to formalize is not merely the invariant that the current value of alloc is closed under the current value of f, but also that all future values of alloc are closed under the current value of f.

Because of the things we have just discussed, the logic includes the function

where fClosedTime(f) is a time beyond which all allocation times are closed under f: Like the axioms about the types of fields and array elements, this axiom does not have an antecedent restricting the values at which maps are applied.  For each field identifier f, the translation assumes as part of the precondition of the method being checked, after each method call that modifies f, and as an invariant of every loop that modifies f.

Note that we could instead have introduced the predicate isFieldClosed mentioned above, but with the axiom:

Then the solid-bulleted axiom and translation assumption above could have been written using isFieldClosed.  Since we see no need to use isFieldClosed as a triggering pattern, it seems more straightforward to use < directly.  (Note that the solid-bulleted axiom does use isAllcoated in a trigger.  This is why we include the function isAllocated in the logic, instead of replacing it every with its definition.)

3.2  Closure of allocatedness under array access

The preceding subsection introduced machinery that formalizes the language invariant that f[x] is allocated whenever x is allocated.  We use similar machinery to formalize the invariant that elems[a][i] is allocated whenever a is allocated.

The logic includes the function

and the axiom The translation assumes as part of the precondition of the method being checked, after each method call that modifies elems, and as an invariant of each loop that modifies elems.

4  Locking

ESC/Java checks for race conditions and deadlocks.  The translation introduces a global map variable LS, called the lock set, that characterizes the set of locks held by the current thread; a lock mu is held whenever LS[mu] == boolTrue.  (Recall that in Java, a lock is exactly the same thing as an object.)  To check for race conditions, the programmer supplies annotations telling which shared variables are protected by which locks.  Whenever a shared variable is accessed and it is necessary to check whether its lock mu is in the lock set, the translation generates the check To check for deadlocks, the programmer supplies annotations defining a relation lockLess (written as < in annotations) on locks: This lockLess relation is transitively closed: Esc/Java verifies that locks are only acquired by any thread in ascending order. If the lockLess order is acyclic, then this guarantees absence of deadlock. (If the programmer erroneously specifies a cyclic ordering, then deadlock may result, but no other error-checking property of ESC/Java is affected.)

It is convenient to assume the invariant that LS has a maximal element.  To see that this assumption is sound, note that the existence of a maximal element follows if LS is totally ordered, finite, and nonempty.  Since LS can be extended only by the acquisition of a lock greater than all locks currently held, and since a method can acquire only one new lock at a time, it follows that if LS is initially totally ordered and finite, it will remain so throughout the execution of any ESC/Java-legal program.  Finally, it is harmless to assume that LS initially contains a sentinel element smaller than any lock acquired during the execution.

To reason about which variables denote lock sets, the logic includes a function

and the translation assumes as a precondition of the method being checked that LS is a valid lock set: In addition, the logic includes a function for extracting the maximum of a lock set: The translation assumes as a precondition of the method being checked that every lock in the lock set is allocated:  WHY??? Since there are no unmatched acquires or releases in Java, the value of LS is left unchanged by method calls and loops.  Hence, there is no reason to repeat this assumption later in the translation of the method being checked.

The translation generates

as a precondition of every call to a synchronized non-static method, and generates as a precondition of every call to a synchronized static method of a class T.  If the method being checked is synchronized, then the translation assumes the precondition if the method is non-static and if the method is a static method of class T.
 
A synchronized block

    synchronized (mu) { S }

is translated into the guarded command

The assumption is used to check calls and synchronized blocks within S.  The assumption is used to check shared-variable accesses in S.  The function store is explained in Section 0.4.

5  Domain-specific axioms

Pretty much every occurrence of a built-in operator of Java gives rise to an occurrence of a corresponding function in the translation.  For many of these functions, there are no axioms specifying their semantics, at least in the initial version of ESC/Java.  This section explains those functions that are given a semantics.

5.0  Properties of arrays

A deference of the length field of an array is translated into an application of the function arrayLength: Every array length is a non-negative int: The rest of this subsection describes four functions and one predicate used to simplify the translation of Java's new operator on array types, including multi-dimensional array types: The functions shapeOne and shapeMore construct array shapes.  Intuitively, a shape is a nonempty list of integers, representing the dimensions of a rectangular array.  For example, shapeOne(6) would be the shape of a one-dimensional array of length 6, and shapeMore(12, shapeOne(7)) would be the shape of a two-dimensional array of length 12, each of whose elements is a one-dimensional array of length 7.

Execution of the Java construct new T[E1][E2]...[En] allocates 1 + 1*E1 + 1*E1*E2 + ... + 1*E1*E2*...*E(n-1) distinct arrays.  The functions arrayParent and arrayPosition are used to ensure that these arrays are in fact distinct, as described below.

The translation of the Java construct new T[E1][E2]...[En] includes an assumption like

where a is the newly allocated array, alloc and alloc' are the allocation times just before and after the allocation of a, elems is the global variable modeling the state of all arrays (see Section 2.5), and zero is the zero-equivalent value of type T.

Informally, the predicate arrayFresh(a, aa, bb, e, s, T, v) states that a is a non-null array allocated between the allocation times aa and bb, of type T and shape s, whose leaf elements in e are v.  By "leaf elements in e", we mean values of the form e[a][i] in case s is a one-dimensional shape, values of the form e[e[a][i]][j] in case s is a two-dimensional shape, etc.  Formally, arrayFresh is defined by the following axioms:

Note that these axioms contain nested quantifications, which themselves have triggering patterns.  Note also that the inner quantifications do not include antecedents requiring that i be in bounds.  As we have remarked before, we believe that this treatment is harmless to the soundness of the logic, and may be beneficial to prover efficiency.

To see how the use of the functions arrayParent and arrayPosition ensure that the arrays allocated as part of a multi-dimensional array allocation are distinct, consider the following program fragment:

    int[][][] a = new int[10][10][10];
    /*@ assert a[3] != a[4]; */
    /*@ assert a[3][7] != a[4][7]; */
    /*@ assert a[3] != a[4][7]; */

The translation and the logic together ensure, after the allocation, that arrayPosition(elems[a][3]) == 3 and that arrayPosition(elems[a][4]) == 4, so when the prover considers the possibility that the first assertion fails (that is, that elems[a][3] == elems[a][4]), it will derive the contradiction 3 == 4.  The translation and logic also ensure that arrayParent(elems[elems[a][3]][7]) == elems[a][3] and that arrayParent(elems[elems[a][4]][7]) == elems[a][4], so when the prover considers the possibility that second assertion fails, it will derive elems[a][3] == elems[a][4], which leads to the contradiction 3 == 4 as just explained.  Finally, the translation and logic ensure that typeof(elems[a][3]) == array(array(int)) and that typeof(elems[elems[a][4]][7]) == array(int).  As discussed in Example 0 of Appendix B, the axioms in Section 1.3 guarantee that the types array(array(int)) and array(int) are distinct, so when the prover considers the possibility that the third assertion fails, it will derive a contradiction.

In Section 2.5, we discussed the possibility of splitting elems into multiple variables (objectElems, intElems, etc.).  Such a change to the logic would complicate these axioms.

5.1  Arithmetic functions on integers

The Java +, -, *, <, <=, ==, !=, >=, and > operators on integers are translated to the corresponding built-in operators of Simplify, which bring Simplify's equality and simplex decision procedures into play.

The Java / and % operators on integers are translated into the functions integralDiv and integralMod, respectively:

Are these axioms and triggers well chosen?

5.2  Reflections of predicates into term space

The next set of axioms we discuss relates to an issue that arises in the translation. The guarded command language makes a strong distinction between predicates and terms. A guard must be a predicate; the right-hand side of an assignment is a term.  Simplify maintains a similar separation; it defines built-in predicates, and everything else is a term.  Java, on the other hand, makes no such strong distinction. The condition of a conditional statement is just an expression of type boolean; the same expression could occur on the right-hand side of an assignment.  Consequently, depending on the context in which a Java expression occurs, its translation produces either a predicate or a term.  For example, the guard of the Java statement

    if (x < y) { ... }

can translate into the predicate x < y, while the right-hand side of the assignment statement

    b = x < y;

must translate into a term intLess(x, y).  The function intLess (axiomatized below) is a reflection of < into the term space.  The logic includes the following functions reflecting Java operators that produce booleans:

In this section, we discuss these functions and their axiomatizations.

5.2.0  Reflected boolean connectives

We start by describing a design decision related to the treatment of booleans.  Recall that in Section 2.2.0 we remarked that we hesitated to include the axiom for fear that it would lead to irrelevant case splits.  Therefore, we take a different approach.  Instead of assuming that there are only two values of type boolean, we axiomatize the reflected versions of the boolean connectives in such a way that the value boolTrue corresponds to the Java predicate true, and all values distinct from boolTrue correspond to the Java predicate false. (Recall that some occurrences of == denote Simplify's built-in predicate symbol EQ and other denote Simplify's built-in boolean connective IFF.  Also recall that Simplify allows applications of user-defined predicate symbols to be used syntactically either as terms or as predicates.  In the case of the latter, Simplify implicitly compares them with boolTrue.  For clarity, since our focus in this section is to describe reflections into term space, we use the functional form.)

5.2.1  Reflected integer and object comparisons

To compare objects or integers for equality, the translator to Simplify generates the Simplify predicates EQ, < etc.
The Java operator instanceof is reflected by the user-defined predicate symbol is, which we have already described in Section 2.0. b

5.2.2  Reflected floating-point comparisons

Comparing floating-point values is not the same as comparing integers, for two reasons.  For one thing, the Java expression r == r, where r is a Java float or double, sometimes doesn't evaluate to true, since r may be NaN (Not-a-Number).  The other difference arises from an infelicitous feature in the implementation of Simplify, described in a digression in Section 2.2.1.  Thus, it is untenable to axiomatize floatingEQ, floatingLE, and floatingLE in the obvious way: We could include such axioms as and axioms relating floatingEQ, floatingLE, and floatingLE to the floating-point arithmetic functions.  However, we propose to omit all such axioms from the initial version of ESC/Java and to add them only as the need becomes evident.

5.2.3  Lifting predicate terms to predicate space

When a Java boolean variable b occurs in a context where a Java predicate is expected, as in the program fragment

    if (b) { ... }

the translation into guarded commands lifts the boolean term b into predicate space by comparing it to boolTrue:

When a boolean expression occurs in such a context, we have a choice of how much of the "computation" to do in predicate space and how much to do in term space.  For example, we might translate

    if (b && x < y) { ... }

in any of the following ways:

A description of the exact translation algorithm, which also includes treatment of short-circuit boolean operators and expressions with side effects, is beyond the scope of this document.

In order to avoid the need to lower predicates into term space, users are not allowed to use genuine predicate expressions (namely, quantified expressions) as subexpressions of terms.  For example, specifications cannot contain expressions like

As it happens, we plan not to allow users to explicitly write store at all.  However, see the discussion of the conditional operator in the next section.

5.3  Reflecting the conditional operator

Occurrences of the Java conditional operator ? : in executable Java code pose no problems--the translation can handle these just as it handles short-circuit boolean operators and expressions with side effects.  On the other hand, occurrences of the conditional operator in specifications will in general require a reflected operator. An alternative would be to write the one axiom Which is best?

Since we are introducing the function termConditional for use in the translation of specifications, the translation of executable code may also benefit from using it.

Note that if the boolean expression B in the specification expression B ? X : Y is allowed to contain a quantified expression when the types of X and Y are not boolean, then the translation will be rather difficult since quantified expressions are fundamentally predicates and there is no direct mechanism for lowering predicates into term space.  We therefore propose to restrict conditional expressions from containing such guards.

5.4  Other domain specific axioms

There is a host of standard Java library classes, such as String, Thread, and Reflection, whose specifications, one can imagine, would require extending the logic of ESC/Java with more functions and axioms.  We don't know to what extent we will need to specify these classes in order to do useful extended static checking of their clients.  For example, to prove that the program fragment

    ch = "hello".toCharArray()[2];

doesn't cause an array index out-of-bounds error, we may need to introduce a function stringLength in order to specify the method String.toCharArray and also to provide special treatment for String literals in the translation of Java to guarded commands.  Other examples may require an axiomatization of stringLength that says that all String lengths are non-negative.  We propose to add such functions and axioms only as the need becomes evident.

Appendix A:  List of predicates, functions, and constants

From Section 0.4, Maps: From Section 1.0, Types: From Section 1.1, The subtype predicate: From Section 1.2, Disjointness of incomparable classes: From Section 1.3, Array types: From Section 2.0, The is predicate: From Section 2.1, Casting: From Section 2.2.0, Booleans: From Section 2.2.1, Integers: From Section 2.3, Types of objects: From Section 2.4, Types of instance variables: From Section 2.5, Types of array elements: From Section 3.0, Allocation times of objects: From Section 3.1, Closure of allocatedness under field access: From Section 3.2, Closure of allocatedness under array access: From Section 4, Locking: From Section 5.0, Properties of arrays: From Section 5.1, Arithmetic functions on integers: From Section 5.2, Reflections of predicates into term space: From Section 5.3, Reflecting the conditional operator:

Appendix B:  List of motivating examples

Example 0

This example is out-of-date, and may no longer be relevant.

We give an example to motivate the axioms in Section 1.3 that distinguish primitive types from array types, such as

Consider the program fragment

    a[i][j] = 6;
    /*@ assert a[i][j] == 6; */

where a is a variable of type a[][].  The translation turns this into a guarded command like

(For simplicity, we have left out the bounds checks.)  The verification condition associated with this guarded command is: Suppose we know elems[a][i] != a.  Then, we can simplify the red underlined select expression to: so that the entire verification condition becomes: Since elems[a][i] == elems[a][i], we can now simplify another select of store expression, reducing the verification condition to: Since j == j, this reduces to: which is true.

But we needed elems[a][i] != a.  We have that typeof(elems[a][i]) == array(int), whereas typeof(a) == array(array(int)).  Hence, it suffices to know that these two types are different.

We end by showing how the axioms from Section 1.3 can help.  Suppose that Simplify explores a potential satisfying assignment in which the two types are postulated to be equal:

By the Section 1.3 axiom we know that and From 0, it follows by congruence closure that and from 2, 3, and 4, it follows that From 2 and 5, we have From 5 and 6, we have contradicting the axiom given in Section 1.3.

Notice that to do the verification in this example, Simplify must consider and refute the case that elems[a][i] != a.  The select of store axiom

will suggest the relevant case split, and give that case split a relatively high priority.  However, we could avoid the case split altogether by changing the logic to split elems into multiple variables, as discussed in a remark in Section 2.5.  If we did so, then the program fragment considered in this example would be translated into the guarded command and the corresponding verification condition would be and the verification can complete with no case splits and without the need for axiom 8.  However, we would still need to perform a case split and to use axiom 8 for a similar example involving a 3-dimensional array.
 

Example 1

We give an example to motivate the final type axioms in Section 1.1. Consider the method:

void f(T[] a, T b) {
   a[0] = b;
}

Verifying this method requires ensuring that b is a subtype of the element type of a (which is non-trivial, since the element type of a may be a subtype of T). Simplify is given that:

    typeof(a) <: array(T)
    typeof(b) <: T

and needs to prove that:

    typeof(b) <: elemType(typeof(a))

From the array axiom triggered on the first antecedent, we have:

    typeof(a) == array(elemType(typeof(a))) &&
    elemType(typeof(a)) <: T

If T is a final type, then the final type axiom is triggered, and yields that:

    elemType(typeof(a)) == T

and then the second antecedent yields the desired consequent.

Example 2

Considering the following variant of example 1:

void f(T[][] a, T[] b) {
   a[0] = b;
}

Verifying this method requires ensuring that b is a subtype of the element type of a (which is non-trivial, since the element type of a may be a subtype of T). Simplify is given that:

    typeof(a) <: array(array(T))
    typeof(b) <: array(T)

and needs to prove that:

    typeof(b) <: elemType(typeof(a))

From the array axiom triggered on the first antecedent, we have:

    typeof(a) == array(elemType(typeof(a))) &&
    elemType(typeof(a)) <: array(T)

From the array axiom triggered on the last line, we have:

    elemType(typeof(a)) == array(elemType(elemType(typeof(a)))) &&
    elemType(elemType(typeof(a))) <: T

If T is a final type, then the final type axiom is triggered, and yields that:

    elemType(elemType(typeof(a))) == T
    elemType(typeof(a)) == array(T)

and hence the desired consequent holds. Note that one affect of the array axiom is to state that arrays of final classes are final.

Example 3

Considering the following example (from test8/trycatch2.java)

class Try2 {
  void m1() throws Throwable {
    int x,y;
    Throwable t;
    try {
      x=0;
      //@ assume typeof(t) == type(Throwable)
      //@ assume t != null
      throw t;
    } catch(RuntimeException t3) {
      x=3;
    }
    //@ assert x==0
  }
}

To verify this class, Esc/Java needs to prove that

    not( Throwable <: RuntimeException )

This motivates the need for the antisymmetry axiom.
 

Appendix C:  List of possible experiments

Legal Statement Privacy Statement