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
foo : Predicate[bar x gorp]
to show that we intend to use the function symbol
foo : bar x gorp --> value
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:
-
(ALL x :: times(e, x) == x)
-
(ALL x :: times(inv(x), x) == e)
-
(ALL x, y, z :: times(x, times(y,
z)) == times(times(x, y), z))
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
-
(ALL x :: times(e, x) == x)
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
-
(ALL x :: times(e, x) == x)
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
-
(ALL s, t, x :: member(x, s)
&& subset(s, t) ==> member(x,
t))
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)}:
-
(ALL s, t, x :: member(x, s)
&& subset(s, t) ==> member(x,
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:
-
(ALL s, t, x :: member(x, s)
&& subset(s, t) ==> member(x,
t))
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
-
Definition: (ALL args :: P(args) == ...)
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
-
(ALL x: X, y :: P(x, y)
==> Q(x, y))
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:
-
(ALL x, y :: isX(x) && P(x,
y) ==> Q(x, y))
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
-
(ALL x, y :: P(asX(x), y)
==> Q(asX(x), y))
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
-
(ALL x :: isX(x) == (x == asX(x)))
or characterize asX by the axioms
-
(ALL x :: isX(x) ==> x == asX(x))
-
(ALL y :: isX(asX(y)))
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
-
(ALL x, y, z :: isXwrtZ(x, z)
&& P(x, y, z) ==> Q(x,
y, z))
we may introduce a function asXwrtZ, assume x == asXwrtZ(x,
z) when we would have assumed isXwrtZ(x, z),
and write the axiom as
-
(ALL x, y, z :: P(asXwrtZ(x,
z), y, z) ==> Q(asXwrtZ(x, z),
y, z))
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:
. [ . ] : map x value --> value
store : map x value x value --> map
The [ ] function is sometimes called select. The semantics
of [ ] and store are given by the following axioms:
-
(ALL m, i, x :: store(m, i,
x)[i] == x)
-
(ALL m, i, j, x :: i != j ==>
store(m, i, x)[j] == m[j])
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:
boolean : type
char : type
byte : type
short : type
int : type
long : type
float : type
double : type
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:
-
DISTINCT(Object, boolean, char, byte, short,
int, long, float, double, Cloneable,
..., String, ..., T, ...)
This axiom is called the Distinct Types Axiom.
1.1 The subtype predicate
The logic includes a subtype predicate:
<: : Predicate[type x type]
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:
-
(ALL t :: t <: t)
-
(ALL t0, t1, t2 :: t0 <: t1
&& t1 <: t2 ==> t0 <: t2)
The subtype relation is also antisymmetric.
-
(ALL t0, t1 :: t0 <: t1 &&
t1 <: t0 ==> t0 == t1)
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
-
(ALL t :: C <: t ==> t == C || D
<: t || J <: t || K <: t ||
...)
For the built-in class Object, this would yield
-
(ALL t :: Object <: t ==> t == Object)
Do we need this?
For each interface declaration
interface I extends J, K, ...
we add the following axioms:
-
I <: Object
This is redundant, but probably not harmful, if the the
interface declaration bears an explicit extends clause.
-
I <: J
-
I <: K
-
...
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:
-
(ALL t :: t <: T == (t == T))
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:
classDown : type x type --> type
asChild : type x type --> type
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
-
(ALL t0, t1, t2 :: t0 <: t1
&& isDirectSubclass(t1, t2) ==> classDown(t2,
t0) == t1)
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
-
(ALL t0, t1, t2 :: t0 <: asChild(t1,
t2) ==> classDown(t2, t0) == asChild(t1,
t2))
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:
-
(ALL t :: array(t) <: 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
-
(ALL t :: ! (array(t) <: T))
This is not implemented because it is not clear we need
to reason about the not-subtype relation.
Technically, we need this axiom only for direct subclasses
of Object, direct subinterfaces of Cloneable, and direct
subinterfaces of Object other than Cloneable.
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:
-
(ALL t :: elemType(array(t)) == t)
Is this the right pattern?
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
-
(ALL t :: isArrayType(t) == (t == array(elemType(t))))
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.
-
(ALL t0, t1 :: t0 <: array(t1)
== (t0 == array(elemType(t0)) && elemType(t0)
<: t1))
2 Types of values
2.0 The is predicate
To reason about the dynamic types of values, the logic includes the following
predicate:
is : Predicate[value x type]
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:
cast : value x type --> value
-
(ALL x, t :: is(cast(x, t),
t))
If the value is already of the specified type, then casting leaves it unchanged:
-
(ALL x, t :: is(x, t) ==> cast(x,
t) == x)
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:
boolFalse : value
boolTrue : value
In fact, these are the only boolean values. We could express this
fact with the axiom
-
(ALL x :: is(x, boolean) == (x
== boolFalse || x == boolTrue))
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:
longFirst : value
intFirst : value
intLast : value
longLast : value
and the following axioms:
-
(ALL x :: is(x, char) == (0 <= x
&& x <= 65535))
-
(ALL x :: is(x, byte) == (-128 <=
x && x <= 127))
-
(ALL x :: is(x, short) == (-32768 <=
x && x <= 32767))
-
(ALL x :: is(x, int) == (intFirst
<= x && x <= intLast))
-
(ALL x :: is(x, long) == (longFirst
<= x && x <= longLast))
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?
Digression. The axioms above
may seem unsound given that not all numbers between, say, -32768 and 32767
are integers: If we translated the Java expression 2.0 < x
&& x < 3.0 (where x is a Java float)
directly into 2 < x && x < 3 (where < is
Simplify's built-in comparison operator), then the axioms above would let
us conclude is(x, int), which would be bad.
To avoid this problem, we considered introducing a predicate isMathInt
to characterize the mathematical integers and writing the axioms above
as:
-
(ALL x :: is(x, char) == (0 <= x
&& x <= 65535 && isMathInt(x)))
-
...
We have rejected this approach on account of an infelicity
in the implementation of Simplify: Simplify's complete decision procedure
for rational linear inequalities is extended by an incomplete heuristic
for integer inequalities. Unfortunately, this heuristic is applied
indiscriminately rather than only to terms that are somehow designated
as integers. For example, Simplify will find the conjunction 2 <
x && x < 3 to be inconsistent, even if x
corresponds to a Java float. Consequently, translating Java's
floating-point < to Simplify's built-in < is untenable even with
isMathInt. We have chosen to give a quite weak axiomatization
of Java's floating point operators (see Section
5.2.2), and in particular to use Simplify's built-in comparison operators
only for integers. Therefore, we see no need for isMathInt.
We could, of course, include isMathInt anyhow, for aesthetics, but
we would then need to include such axioms as
-
(ALL x, y :: isMathInt(x) && isMathInt(y)
==> isMathInt(x + y))
and to generate the assumption isMathInt(c)
for every integer literal c occurring in the program. (End
of Digression.)
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
-12000000
72000
800000
12000000
123456789
1234567890123456789L
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:
-
longFirst < intFirst
-
intFirst < neg12000000
-
neg12000000 < -1000000
-
1000000 < pos12000000
-
pos12000000 < pos123456789
-
pos123456789 < intLast
-
intLast < pos1234567890123456789
-
pos1234567890123456789 < longLast
Note that in the absence of such large constants, we will have the following
axioms:
-
longFirst < intFirst
-
intFirst < -1000000
-
1000000 < intLast
-
intLast < longLast
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.
-
(ALL x :: is(x, int) ==> is(x,
double))
What is the trigger?
-
(ALL x :: is(x, float) ==> is(x,
double))
What is the trigger?
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:
-
(ALL x, t :: t <: Object ==> is(x,
t) == (x == null || typeof(x) <:
t)))
Will this produce useless case splits?
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:
-
this != null && typeof(this) <:
C
2.4 Instantiable types
The dynamic type of a non-null object must be an instantiable
type. The logic could includes a predicate
instantiable : Predicate[type]
and the axiom
-
(ALL x :: instantiable(typeof(x)))
Is this the right trigger?
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:
asField : map x type --> map
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
-
(ALL f, t, x :: is(asField(f,
t)[x], t))
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:
-
(ALL e, a, i :: is(asElems(e)[a][i],
elemType(typeof(a))))
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
isAllocated : Predicate[value x time]
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():
! isAllocated(result, alloc) && isAllocated(result,
alloc')
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:
assume isAllocated(x, alloc) &&
... ;
var y in
assume y == null ;
var result, alloc' in
assume ! isAllocated(result,
alloc) && isAllocated(result, alloc')
&& ... ;
alloc = alloc'
;
y = result
end ;
assert x != y
end
The verification condition for this piece of code is:
isAllocated(x, alloc) && ... ==>
(ALL y :: y == null
==>
(ALL result, alloc'
:: ! isAllocated(result, alloc) && ...
==>
x != result ))
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:
-
(ALL v :: isAllocated(v, alloc) ==>
isAllocated(v, 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:
vAllocTime : value --> time
Third, we define isAllocated in terms of vAllocTime and Simplify's
built-in < operator:
-
Definition: (ALL x, aa :: isAllocated(x,
aa) == (vAllocTime(x) < aa))
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:
-
(ALL x, f, aa :: isFieldClosed(f, aa)
&& isAllocated(x, aa) ==> isAllocated(f[x],
aa))
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
fClosedTime : map --> time
where fClosedTime(f) is a time beyond which all allocation
times are closed under f:
-
(ALL x, f, aa :: fClosedTime(f) <
aa && isAllocated(x, aa) ==> isAllocated(f[x],
aa))
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:
-
(ALL f, aa :: isFieldClosed(f, aa)
== fClosedTime(f) < aa)
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
eClosedTime : map --> time
and the axiom
-
(ALL a, e, i, aa :: eClosedTime(e)
< aa && isAllocated(a, aa) ==> isAllocated(e[a][i],
aa))
The translation assumes
-
eClosedTime(elems) < alloc
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
assert LS[mu] == boolTrue
To check for deadlocks, the programmer supplies annotations defining a
relation lockLess (written as < in annotations) on locks:
lockLess : Predicate[value x value]
This lockLess relation is transitively closed:
-
(ALL x0,x1,x2 :: (lockLess x0 x1) && (lockLess x1 x2)
=> (lockLess x0 x2))
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:
lockSetMax : map --> value
-
(ALL S :: asLockSet(S)[lockSetMax(asLockSet(S))]
== boolTrue)
The translation assumes as a precondition of the method being checked that
every lock in the lock set is allocated: WHY???
-
(ALL mu :: LS[mu] ==> isAllocated(mu,
alloc))
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
-
lockLess(lockSetMax(LS), this) || LS[this]
== boolTrue
as a precondition of every call to a synchronized non-static method, and
generates
-
lockLess(lockSetMax(LS), T) || LS[T]
== boolTrue
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
assert lockLess(lockSetMax(LS),
mu) || LS[mu]
== boolTrue ;
var oldLS in
assume oldLS
== LS ;
var newLS in
assume
(lockLess(lockSetMax(LS), mu) && mu
== lockSetMax(newLS)) ||
(LS[mu] == boolTrue && newLS == LS)
;
assume
newLS == store(LS, mu,
boolTrue) ;
assume newLS == asLockSet(newLS)
;
LS
= newLS ;
S
(* actually, the translation of S *)
end ;
LS = oldLS
end
The assumption
assume (lockLess(lockSetMax(LS),
mu) &&
mu == lockSetMax(newLS))
||
(LS[mu]
== boolTrue && newLS == LS)
is used to check calls and synchronized blocks within
S. The assumption
assume newLS == store(LS,
mu, boolTrue)
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:
arrayLength : value --> value
Every array length is a non-negative int:
-
(ALL a :: 0 <= arrayLength(a) &&
is(arrayLength(a), 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:
shapeOne : value --> shape
shapeMore : value x shape --> shape
arrayParent : value --> value
arrayPosition : value --> value
arrayFresh : Predicate[value x time x time x map
x shape x type x value]
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
-
arrayFresh(a, alloc, alloc', elems,
shapeMore(E1, shapeMore(E2, ...(shapeOne(En))...)),
array(array(...(array(T))...)),
zero)
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:
-
(ALL a, aa, bb, e, n, s, T,
v ::
arrayFresh(a, aa,
bb, e, shapeMore(n, s), T, v)
==
aa <= vAllocTime(a)
&& vAllocTime(a) < bb &&
a != null
&& typeof(a) == T && arrayLength(a)
== n &&
(ALL i ::
arrayFresh(e[a][i], aa, bb,
e, s, elemType(T), v) &&
arrayParent(e[a][i]) == a &&
arrayPosition(e[a][i]) == i))
-
(ALL a, aa, bb, e, n, T, v
::
arrayFresh(a, aa,
bb, e, shapeOne(n), T, v)
==
aa <= vAllocTime(a)
&& vAllocTime(a) < bb &&
a != null
&& typeof(a) == T && arrayLength(a)
== n &&
(ALL i :: e[a][i]
== v))
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:
integralDiv : value x value --> value
integralMod : value x value --> value
-
(ALL i, j :: integralDiv(i, j) * j
+ integralMod(i, j) == i)
-
(ALL i, j :: 0 < j ==> 0 <= integralMod(i,
j) && integralMod(i, j) < j)
-
(ALL i, j :: j < 0 ==> j < integralMod(i,
j) && integralMod(i, j) <= 0)
-
(ALL i, j :: integralMod(i + j, j)
== integralMod(i, j))
-
(ALL i, j :: integralMod(j + i, j)
== integralMod(i, j))
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:
boolAnd : Predicate[value x value]
boolOr : Predicate[value x value]
boolNot : Predicate[value]
boolEQ : Predicate[value x value]
floatingEQ : Predicate[value x value]
floatingLE : Predicate[value x value]
floatingLE : Predicate[value x value]
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
-
(ALL x :: is(x, boolean) == (x
== boolFalse || x == boolTrue))
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.
-
Definition: (ALL b, c :: boolAnd(b, c)
== (b == boolTrue && c == boolTrue))
-
Definition: (ALL b, c :: boolOr(b, c)
== (b == boolTrue || c == boolTrue))
-
Definition: (ALL b :: boolNot(b) == (b
!= boolTrue))
-
Definition: (ALL b, c :: boolEQ(b, c)
== ((b == boolTrue) == (c == boolTrue)))
(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:
-
Definition: (ALL x, y :: floatingEQ(x,
y) == (x == y))
-
Definition: (ALL x, y :: floatingLE(x,
y) == (x < y))
-
Definition: (ALL x, y :: floatingLE(x,
y) == (x <= y))
We could include such axioms as
-
Definition: (ALL x, y :: floatingEQ(x,
y) == (! isNaN(x) && ! isNan(y)
&& x == y))
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:
if boolAnd(b, intLess(x, y))
== boolTrue --> ...
if b == boolTrue && intLess(x,
y) == boolTrue --> ...
if b == boolTrue && x < y
--> ...
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
store(myBooleanArray, i, (forall ...))
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.
termConditional : value x value x value --> value
-
(ALL x, y :: termConditional(boolTrue, x,
y) == x)
-
(ALL b, x, y :: b != boolTrue ==> termConditional(b,
x, y) == y)
An alternative would be to write the one axiom
-
(ALL b, x, y :: (b == boolTrue &&
termConditional(b, x, y) == x)
|| (b != boolTrue && termConditional(b,
x, y) == y))
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:
. [ . ] : map x value --> value
store : map x value x value --> map
From Section 1.0, Types:
boolean : type
char : type
byte : type
short : type
int : type
long : type
float : type
double : type
From Section 1.1, The subtype predicate:
<: : Predicate[type x type]
From Section 1.2, Disjointness of incomparable
classes:
classDown : type x type --> type
asChild : type x type --> type
From Section 1.3, Array types:
array : type --> type
elemType : type --> type
From Section 2.0, The is predicate:
is : Predicate[value x type]
From Section 2.1, Casting:
cast : value x type --> value
From Section 2.2.0, Booleans:
boolFalse : value
boolTrue : value
From Section 2.2.1, Integers:
longFirst : value
intFirst : value
intLast : value
longLast : value
From Section 2.3, Types of objects:
typeof : value --> type
instantiable : Predicate[type]
From Section 2.4, Types of instance
variables:
asField : map x type --> map
From Section 2.5, Types of array elements:
From Section 3.0, Allocation times
of objects:
isAllocated : Predicate[value x time]
vAllocTime : value --> time
From Section 3.1, Closure of allocatedness under
field access:
fClosedTime : map --> time
From Section 3.2, Closure of allocatedness under
array access:
eClosedTime : map --> time
From Section 4, Locking:
lockLess : Predicate[value x value]
asLockSet : map --> map
lockSetMax : map --> value
From Section 5.0, Properties of arrays:
arrayLength : value --> value
shapeOne : value --> shape
shapeMore : value x shape --> shape
arrayParent : value --> value
arrayPosition : value --> value
arrayFresh : Predicate[value x time x time x map
x shape x type x value]
From Section 5.1, Arithmetic functions
on integers:
integralDiv : value x value --> value
integralMod : value x value --> value
From Section 5.2, Reflections of predicates
into term space:
boolAnd : Predicate[value x value]
boolOr : Predicate[value x value]
boolNot : Predicate[value]
boolEQ : Predicate[value x value]
floatingEQ : Predicate[value x value]
floatingLE : Predicate[value x value]
floatingLE : Predicate[value x value]
From Section 5.3, Reflecting the conditional
operator:
termConditional : value x value x value --> value
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
-
int != array(elemType(int))
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
elems = store(elems, elems[a][i],
store(elems[elems[a][i]], j,
6)) ;
assert elems[elems[a][i]][j]
== 6
(For simplicity, we have left out the bounds checks.)
The verification condition associated with this guarded command is:
store(elems,
elems[a][i],
store(elems[elems[a][i]], j, 6))
[ store(elems,
elems[a][i],
store(elems[elems[a][i]],
j, 6))
[a][i]
]
[j] == 6
Suppose we know elems[a][i]
!= a. Then, we can simplify the red underlined select
expression to:
so that the entire verification condition becomes:
store(elems,
elems[a][i],
store(elems[elems[a][i]],
j, 6))
[ elems[a][i]
]
[j] == 6
Since elems[a][i] == elems[a][i],
we can now simplify another select of store expression, reducing
the verification condition to:
store(elems[elems[a][i]],
j, 6))
[j] == 6
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:
0. array(int) == array(array(int))
By the Section 1.3 axiom
-
1. (ALL t :: elemType(array(t))
== t)
we know that
2. elemType(array(int))
== int
and
3. elemType(array(array(int)))
== array(int)
From 0, it follows by congruence closure that
4. elemType(array(int))
== elemType(array(array(int)))
and from 2, 3, and 4, it follows that
From 2 and 5, we have
From 5 and 6, we have
7. int == array(elemType(int))
contradicting the axiom
-
8. int != array(elemType(int))
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
-
(ALL m, i, j, x :: i
!= j ==> store(m, i, x)[j]
== m[j])
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
intElems = store(intElems,
objectElems[a][i], store(intElems[objectElems[a][i]],
j, 6)) ;
assert intElems[objectElems[a][i]][j]
== 6
and the corresponding verification condition would
be
store(intElems,
objectElems[a][i],
store(intElems[objectElems[a][i]],
j, 6))
[objectElems[a][i]]
[j] == 6
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