Revisiting the \past

[davidcok]

Here is a quiz for you. Your reward will be a pristine e-copy of JML2nd edition when it ships.

Which of the asserts in the following code should be true and which not:

public class Past {

public static class T {
  public int v;

  //@ ensures \result == (x.v == y.v);
  //@ pure
  static public boolean equals(T x, T y) { return x.v == y.v; }

}
  //@ requires t1.v == 5;
  //@ requires t2.v == 6;
  //@ requires t1 != t2;
  //@ requires t3 == t1;
  //@ requires t4 != t1 && t4 != t2 && t4 != t3 && t4.v == 5;
  static public void m(T t1, T t2, T t3, T t4) {
    t1.v = 15;
    //@ assert \old(t1).v == 15;
    //@ assert \old(t1.v) == 5;
    t2.v = 16;
    t3 = t2;
  Here: ;
    //@ assert t3.v == 16;
    //@ assert \old(t3.v) == 5;
    //@ assert \old(t3).v == 15;
    //@ assert \old(\old(t3,Here).v) == 6;

    //@ assert T.equals(t1, \old(t1));
    //@ assert T.equals(t4, \old(t1));

  }
}

Think about the last two particularly carefully. They can't both be true. All references non null by default.

[mattulbrich]

My answers

I'd say all but the last one pass. Is no 5 well-defined? There is a forward-reference then. But I assume we can define this, too ... probably a pass

[mattulbrich]

What about the following program?

class C { int value; /* + obvious contructor */ }

static void(C c) {
   c = new C(42);
   here:
   //@ assert \old(\old(c, here).value) == 42;
   //@ assert \old(\old(c, here).value) != 42;
}

Exactly one of the assertions should be true.

Or should it?

[wadoon]

This is a design decision, whether \old stacks up.

I would say \old(\old(x)) is equals to \old(x), so I would go for

//@ assert \old(\old(c, here).value) == 42;

Otherwise, I see well-definedness problems when one uses so many \old that a heap is referenced before the method/program was executed:

boolean x = true;
public void foo() { 
  //@ assert \old(\old(x));
}

[davidcok]

At present in JML, \old can be nested. One view is to say that Mattias's examples are not well-defined. That is, one is not allowed to access the fields of an object before the constructor begins to execute.

The other view is to say that all objects that ever will be constructed 'exist', they just are not reachable until a constructor is called. Then there are two subviews a) the object exists (call it c') but is not initialized, so c'.value is either 0 or arbitrary b) the object exists as it eventually will be initialized, so the value of c'.value is 42. But this view rapidly gets one into trouble if the constructor captures other references which may or may not yet be constructed/initialized themselves.

So in my view either (1) or (2a). As I don't like reasoning or even thinking about not yet but eventually created objects, I'd come down on the side of (1).

[mattulbrich]

So in my view either (1) or (2a). As I don't like reasoning or even thinking about not yet but eventually created objects, I'd come down on the side of (1).

KeY follows the principle of "underspecification", i.e. any expression has a value (even 1/0), but for expressions that evaluate outside the operators domain (like division by zero or heap access on not-yet-created objecte) the value remains underspecified, undefined, arbitrary.

So, I'd say: The example is not well-defined since the "." operator works on a not-yet-created object. If one skips this well-definedness argument, then I'd say the value is unspecified. Neither assertions is valid.

I agree with David that it would become ugly if in the trouble cases he mentions.

Btw. one does not need old-with-label and can also do:

 //@ assert (\forall C x; x == c; \old(x.value) == 42);

for the 1st assertion and reach the same problem.

[davidcok]

But here is the real reason I posed this quiz. The asserts are all just warmup for the last two. What happens when an argument of a method is an \old expression. Mattias's answers agree with classic JML. But consider a case where T is a non-empty linked list, so that an instance of T is a reference to the head of the list.

Then

{ T my list = ...
a:
...
  my_list.append(v);
b:
  assert equals(\old(my_list,a),\old(my_list,b));
}

In both the a and b states, my_list points to the same head, so the equals is evaluated with identical elements. The body of (or the spec of) the equals evaluates all the '.' operations to compare the lists in the current state, and the result is that the assert is true.

But the intent is very likely to compare the whole list as it is in the current state b with the list evaluated in state a, that is with all the '.' operations evaluated in state a.

This was the topic of a discussion at the Shonan JML workshop in 2013 [amazingly, I still have email exchanges about it]. There the feature \past was proposed, which is like old, but the state/heap carries along with a reference to the dot- and array operations subsequently performed on the reference. That way the chosen heap/state propagates into the evaluation of expressions within the spec of the method call. The feature was adopted into JML but not ever implemented in tools (at least by me).

So then assert T.equals(t4,\past(t1)); would be true.

The paper authors claimed that this was actually a preferable semantics for \old and closer to what the user generally intended. My caveat is that there is a clear difference in intention between \old(t.v) and \old(t).v, which is lost if one replaces \old by \past.

A particular caution is that this is not easy to evaluate in RAC; one essentially needs to have a copy of the heap in which to evaluate dot-operations on references. However, one of the papers at that workshop did show an efficient (though by no means trivial) implementation to do just that.

Plus there could semantic issues lurking in comparing things across heaps.

Nevertheless this was the justification then for \past. The question for JML2ndEdition is whether we stick with that past decision.

Gary - you were there. Anything to add? Or DMZ, if you are listening?

[mattulbrich]

On 14.12.21 01:08, David Cok wrote:

The paper authors claimed that this was actually a preferable semantics for \old and closer to what the user generally intended.

Do you have a link to the paper?

I have a bias to seeing things the KeY-way, but I this does unfortunately not fit into my understanding of things.

A reference points to an object identity, the address. It does not contain the actual data of that object.

T.equals receives two pointers, not two data structures.

---

On a related issue:

KeY has so-called "two-state" model methods, which is a little related. You can write:

class C { int value; }

/*@ model two_state increasedValue(C c) {
  @      return c.x > \old(c.x);
  @ } */

/*@ ensures increasedValue(c); */
void inc(C c) { c.value++; }

[mattulbrich]

But the intent is very likely to compare the whole list as it is in the current state b with the list evaluated in state a, that is with all the '.' operations evaluated in state a.

Then we should not compare the references but go and retrieve their state as a value and compare that. In KeY, we use \seq for sequences, it should be essentially the same as one of JML model classes.

interface List {
   //@ instance model \seq values;

   //@ ensures values == \seq_append(\old(values), v);
   void append(int v);

   // other methods ...
}

{ T my list = ...
a:
...
  my_list.append(v);
b:
  assert equals(\old(my_list.values,a),\old(my_list.values,b));
}

Now, \old does the trick very nicely.

[davidcok]

A reference points to an object identity, the address. It does not contain the actual data of that object. A Java and JML viewpoint that matches mine. The question is how to get at what the proposers of \past wanted. Here is a reference to their paper: https://dl.acm.org/doi/10.1145/2451436.2451453 (Thanks Gary for preserving the reference)

And regarding Mattias's example above, I entirely concur that this is a way to solve the problem that fits in well with the current JML and with the JML-way of modeling things -- namely, to have model fields that 'model' the relevant value of an object as primitive value-semantics data types.

And for that we have to expand the library of types etc. that users can use to do that -- not just collection types but tuples and record-like datatypes as well.

But this inclines me to drop \past, though I don't feel strongly. And note that either keeping or deprecating it will require careful education of users.

[mattulbrich]

I have checked out the paper. I do like the idea and have one or two problems in mind where this technique might have helped indeed. However, it breaks with JML+Java basic builtin concept of call by reference by implementing a verification-only call-by-value. It will confuse beginners profoundly if we have both. It would be cool to have that around for some research experiments, but I would also drop it from the ref manual(, respectively not add it.)

There is a similar thing called \other in relational regression verification. Totally convenient. But I would not put it into the ref man.

Sounds like consesus? @leavens

[dmzimmerman]

It will confuse beginners profoundly if we have both.

I'm not sure about that. This particular proposal was near to my heart (though I had nothing to do with developing it) precisely because of the difficulty of explaining to beginners how they could build up JML specifications to do this sort of thing, and why they couldn't just compare arbitrary complex objects in the pre-state with those in the post-state. I myself have, many times, wanted to be able to use this technique in specifications - primarily, as one might expect, having to do with reasoning about transformations done on collections or arrays. JML specifications are not actually executable Java (RAC notwithstanding; as David said, this would require a decent amount of work to be handled properly by RAC), and I think it makes a lot of sense to have something like \past available to concisely describe such heap transformations. They certainly can be described by using model fields, or by retrieving the individual elements in both the pre- and post-states and comparing those, but that, it seems to me, is a lot harder for beginners than having a working \past would be. It also leads to specifications that are much less concise and readable, even for simple things; compare (just off the top of my head):

// a list is not modified
@ensures list.size() == \old(list.size()) && (\forall i; 0 <= i < list.size(); list.get(i).equals(\old(list.get(i))));

with

// a list is not modified
@ensures list.equals(\past(list));

Even if you do the equivalent of the first with model fields, it's significantly more cumbersome. Especially for beginners.

[dmzimmerman]

David wrote pretty far up above here:

The paper authors claimed that this was actually a preferable semantics for \old and closer to what the user generally intended. My caveat is that there is a clear difference in intention between \old(t.v) and \old(t).v, which is lost if one replaces \old by \past.

I agree with the "closer to what the user generally intended" wholeheartedly... and while it's true that there is a clear difference in intention between \old(t.v) and \old(t).v, I wonder how often the need for such a difference of intention arises specifically because of not having a way to express \past.

Of course, \old doesn't really have to be replaced by \past, either; they could coexist.

[leavens]

Technically, Java (and JML) use call by value, but the values of objects are references (sometimes this is called call-by-value with the reference model).

About the consensus, to just have \old in JML but not \past yet, that makes sense to me. It seems easier to implement \old in Java than \past.

However, I do definitely see advantages to the \past mechanism, but it makes sense to leave it for the future.

[mattulbrich]

I concur this Gary's view. Let's not solve all problems at once and keep that on a future-list.

However, I do definitely see advantages to the \past mechanism, but it makes sense to leave it for the future.

[davidcok]

Agreed. We'll keep the keyword \past for this potential future use, but not make it part of the language for now. An experimental implementation in a tool might give some insight.