[From posts to src.sparta dated 11 Dec 97 and 19 Dec 97.]
At the Sparta meeting today, Greg, Raymie, and I discussed when ESC/Java
should assume and check that object invariants hold. Here is
what
we thought seemed like a good idea. (These rules pertain to non-constructor
methods; constructors have slightly different rules.)
On entry to the method whose body is being checked, assume that
the following objects satisfy their invariants:
* all allocated objects
On exit from the method whose body is being checked, check that the
following objects satisfy their invariants:
* all allocated objects
At a call to a method, check that the following objects satisfy their
invariants:
* all actual in-parameters (including "this") and all global
variables
(aka static fields)
On return from a method call, assume that the following objects satisfy
their invariants:
* every object "x" where "x.f" (for some field "f", possibly
"elems")
occurs in the modifies list of the method being
called, and all objects
that are allocated during the call
<30-minute break>
I just spoke with Cormac about these rules and realized that they
need improvement. Consider the following code fragment:
class C {
int x;
/*@ invariant 0 <= x */
Y y;
/*@ invariant y != null */
void m() {
x = -1;
y.n();
x = 0;
}
...
}
We had hoped that the rules above would allow the body of "C.m" to
check: the invariant of "this" doesn't hold at the call to "y.n()",
but it also doesn't have to, because "C.m.this" is not an actual
parameter to "y.n()". But it might be the contents of a global
variable!
Suppose that this verification is done where the following global
variable is visible:
static Object g;
Then, the rules above would require that invariant of "g" hold at
the call to "y.n()". The prover would not miss this opportunity
to point out the possibility that "g == this".
To solve this problem with the rules given above, one would need
to have a way to conclude that "g" differs from "this". I think
that would end up being a mess. It's probably better to adjust
the
rules above to say something different about global variables.
Rustan
In yesterday's Sparta meeting, we revisited last week's discussion
of which object invariants to check and assume when. Here's an
attempt
at specifying the behavior that we (or at least I) currently think
we should implement. (I have totally changed the formulation
of
the last rule.) I'll try to be more concrete than in my message
from a week ago.
An object invariant is a boolean condition that is written down
in a class. For example, consider the following class.
class C {
int x, y;
/*@ invariant x < y */
T t;
/*@ invariant t != null
*/
...
This class contains two object invariants about the fields of "C"
objects. Expanding out the implicit "this" object, the same code
reads:
class C {
int x, y;
/*@ invariant this.x <
this.y */
T t;
/*@ invariant this.t !=
null */
...
For the rest of this message, I will assume that "this" is always
given explicitly.
I will say "C-invariant" to refer to any object invariant declared
inside class "C".
To avoid unnecessary cases, I will treat the self parameter of
instance methods as being just another ordinary parameter.
I will ignore constructors for now, focusing only on ordinary instance
methods and static methods.
Here we go.
* *
*
Consider the verification of a method "m".
Here's what the ESC/Java tutorial/cookbook would say:
All object invariants of all objects are assumed
at the beginning
of "m" and checked at the end of "m". In addition,
the object
invariants of the actual parameters to a method
"n" and of globals
are checked for every call to "n". The call
to a method "n"
is assumed not to falsify any invariant.
* *
Now for the details.
Just inside the body of "m", the translation (of Java into Guarded
Commands) would generate an assumption
(ALL this: C :: J ) (*)
for every C-invariant "J" (for every "C").
Remark. With the quantification (*), I actually
mean
(ALL this ::
this instanceof C && isAllocated(this, alloc)
&&
this != null
==>
J
)
For the benefit of the uninitiated, let me explain
the first two
conjuncts of the antecedent. Recall that the
logic underlying ESC/Java
is untyped, so the quantification is really over
all values of a
variable conveniently called "this". The first
conjunct of the antecedent
says that the dynamic type of "this" is a subtype
of "C". The second
conjunct in the antecedent states that "this" is
allocated (before
the allocation time "alloc", which in this example
refers to
the time of entry to the body of "m").
To keep things palatable, I will continue to write
quantification in
the form (*). (End of Remark.)
* *
Just before the end of the body of "m", the translation will generate
a check
(ALL this: C :: J )
for every C-invariant "J".
* *
Just before a call to a method "n", the translation will generate
a check
(ALL this: C :: (this == x || this ==
y || ... || this == z)
==> J )
for every C-invariant "J", where for a particular "C" the
"x", "y", ..., "z" are the global variables (that is, static fields)
whose static types are subtypes of "C" and the actual parameters of
"n"
whose static types are subtypes of "C".
(Note that this formula is equivalent to:
J[this := x] && J[this := y] && ... && J[this := z]
Which of the two should we use?)
* *
Just after the invocation of a method "n", the translation will generate
an assumption
(ALL this: C :: J0 || ! isAllocated(this, alloc0) ==> J )
(where "alloc0" and "J0" denotes the values of "alloc0" and "J" before
the call to "n") for every C-invariant "J" that mentions any field
or global variable allowed--on account of a MODIFIES clause--to be
modified by "n".
Rustan