frame conditions and non-disjoint behaviors

[davidcok]

This issue is handled in OpenJML but I can't recall it ever being discussed. So comments welcome.

Given a caller with specification (A and B are sets of locations) requires P; assigns A; also requires Q; assigns B;

that calls a callee with specification requires P; assigns A'; also requires Q assigns B'

If P and Q are disjoint then it must hold that P ==> (A' <= A) and Q ==> (B' <= B) (where <= here is subset of) If P and Q are not disjoint, then naively one might think that the following has to hold (P & !Q) ==> (A' <= A) and (P&Q) ==> (A' <= A & A' <= B & B' <= A & B' <= B) and (!P & Q) ==> (B' <= B) that is, in the case of P&Q (A'+B') <= (AB) (+ is union, is intersection)

However, suppose we refactor the callee's spec into requires P&!Q; assigns A'; also requires P&Q; assigns A'; assigns B'; also requires !P&Q; assigns B';

For P&Q, the fact that both assigns clauses must be independently true, means that together they are equivalent to assigns A'B'; That means that the proof obligation for P&Q is actually (A'B') <= (AB), which is different than and less restrictive than (A'+B')<=(AB) above.

So (a) one must desugar into disjoint behaviors to get this correct and (b) users should be discouraged from having non-disjoint behaviors.

[mattulbrich]

Is this similar to asking if

//@ requires true; assignable this.x;
//@ also requires true; assignable this.y;
void m() {
   n();
}

//@ requires true; assignable this.x, this.y;
void n() { }

is correct?

[leavens]

Yes, I would say it's similar. Each specification case should be obeyed, and thus when one specification case says that one can only assign to x and the other to y, then an implementation cannot assign to either one (it must obey both specifications).

Let me revisit David's example:

requires P;
assignable A;
also
requires Q;
assignable B;
void caller(T o) { o.callee(); }

requires P;
assignable A';
also
requires Q;
assignable B';
void callee();

I think it's easier to regard assignable clauses to be shorthand for postconditions, by using \only_assigned(), so we can say that the above is equivalent to:

requires P;
ensures \only_assigned(A);
also
requires Q;
ensures \only_assigned(B);
void caller(T o) { o.callee(); }

requires P;
ensures \only_assigned(A');
also
requires Q;
ensures \only_assigned(B');
void callee();

And now we can use the desugaring of specification cases, so the above is in turn equivalent to:

requires P || Q;
ensures (\old(P) ==> \only_assigned(A)) && (\old(Q) ==> \only_assigned(B));
void caller(T o) { o.callee(); }

requires P || Q;
ensures (\old(P) ==> \only_assigned(A')) && (\old(Q) ==> \only_assigned(B'));
void callee();

Suppose that P && Q is true in the pre-state, then for the callee to refine the caller's specification, we must have that:

((\old(P) ==> \only_assigned(A')) && (\old(Q) ==> \only_assigned(B')))
==>
((\old(P) ==> \only_assigned(A)) && (\old(Q) ==> \only_assigned(B)))

So, since both\old(P) and \old(Q) are true by assumption, for correctness we need the following:

(\only_assigned(A') && \only_assigned(B'))
==>
(\only_assigned(A) && \only_assigned(B))

In terms of sets, this means that the intersection (A'*B') must be a subset of (A*B) .

[mattulbrich]

I reckon the underlying question behind this is whether contracts are to be statically checked individually, or whether combining of behaviours into a single "master behaviour" happens before verification.

In condensed form: Is the following correct? It probably is since the assertion never fails. (I am afraid KeY would I think not be able to prove this as is since it combines contracts on demand when using them but proves them separately.)

int x;
/*@ requires x < 10;
  @ also requires x >= 0;
  @*/
void m() {
  assert 0 <= x && x < 10;
}

[davidcok]

Mattias's example is not correct. And it is not an example of the original question. Each specification case (a.k.a. behavior) must hold independently when verifying the body of the method. Thus the preconditions are not conjoined as the assert in the above expects. And even when the method is called, only one of the specification cases needs to have a true precondition -- that is, the preconditions of the spec cases are disjoined.

The examples I posed intend to show the non-intuitive behavior of frame conditions when one has non-disjoint spec cases for a called method. Gary's comment and my understanding are in agreement. I'm not sure yet how KeY handles the matter.

[leavens]

I'm happy that you agree with me David (@davidcok), so perhaps this is a case where we agree?

[davidcok]

Not so rare. I mostly was checking for KeY's take

[mattulbrich]

In KeY, it seems to be sufficient to have A' <= A and B' <= B for the initial example.

See the KeY code that verifies:

``` class A { //@ ghost \locset A; //@ ghost \locset A2; //@ ghost \locset B; //@ ghost \locset B2; boolean P; boolean Q; /*@ normal_behaviour @ requires P; @ assignable A, A2; @ also normal_behaviour @ requires Q; @ assignable B, B2; @*/ void outer() { inner(); } /*@ normal_behaviour @ requires P; @ assignable A; @ also normal_behaviour @ requires Q; @ assignable B; @*/ void inner() { } } ```

I am convinced that this is sound.

[leavens]

Mattias, perhaps we are agreeing. If both P and Q are true, then both contracts should be obeyed, so A' <= A and also B' <= B in that case, so the intersection (A'B') must be a subset of `(AB)`. This is in reference to the following example.

requires P;
assignable A;
also
requires Q;
assignable B;
void caller(T o) { o.callee(); }

requires P;
assignable A';
also
requires Q;
assignable B';
void callee();

[mattulbrich]

So, we all agree. Great! :smiley: I assume, no action is needed?