\fresh with labels and \before

[flo2702]

Mattias and I recently had a discussion about the semantics of \fresh on block contracts, and we came to the conclusion that it would be nice to have something like \fresh(var, lbl) (in parallel with \old(var, lbl) in the standard. The semantics of \fresh(var, lbl) would be equivalent to \fresh(var) && !\old(\fresh(var), lbl).

Relatedly, while KeY does not currently support old with labels in general, it does have the keyword \before(var), which always refers to the prestate of the program element the contract belongs to. In other words, it is equivalent to \old(var, lbl0) if lbl0 refers to the current block. So the following specification would be true:

//@ ensures x == \old(x) + 2
void foo() {
    ++x;
     /*@ ensures \before(x) == \old(x) + 1;
       @ ensures x == \before(x) + 1;
       @ ensures x == \old(x) + 2;
       @*/
    { ++x; }
}

In my opinion, this is a convenient piece of syntactic sugar when writing block contracts. But if we include \fresh with labels, maybe we want something more general, like a label current which always refers to the current block. Then we could write:

//@ ensures x == \old(x) + 2
void foo() {
    ++x;
     /*@ ensures \old(x, current) == \old(x) + 1;
       @ ensures x == \old(x, current) + 1;
       @ ensures x == \old(x) + 2;
       @ ensures \fresh(y, current);
       @*/
    { ++x; y = new Object(); }
}

[davidcok]

In current JML \pre refers to the pre-state of the enclosing method and \old is the pre-state of the current contract (is context dependent). So I would have simply written your first example as

//@ ensures x == \old(x) + 2
void foo() {
    ++x;
     /*@ ensures \old(x) == \pre(x) + 1; // or is this a requires?
       @ ensures x == \pre(x) + 2;
       @ ensures x == \old(x) + 1;
       @*/
    { ++x; }
}

[flo2702]

• Regarding \pre and \old: That makes me wonder what the pre-state of a loop spec is: is it the state before the loop was entered for the first time, or the state before the current iteration? In KeY's loop contracts (which are specified with requires and ensures like recursive methods), \before(var) currently refers to the state before the current iteration, since otherwise some loop contracts would not be provable.
• Regarding \fresh: Maybe \fresh(var) should be changed to match \old and refer to the pre-state of the current contract and the case where we want to refer to the pre-state of the method should be the one with the more elaborate syntax instead:

void foo() {
    start:
    y = new Object();
     /*@ ensures \fresh(y); // false
       @ ensures \fresh(y, start); // true
       @ ensures \fresh(z); // true
       @*/
    { z = new Object(); }
}

I can't think of any use cases where I would actually want to write something like \fresh(y, start), so this might be the better default. But on the other hand, it makes it impossible to consider \fresh(var, lbl) as simply syntactic sugar for something like \fresh(var) && !\old(\fresh(var), lbl).

[leavens]

It seems good to have \fresh have a semantics that is very similar to \old, especially with respect to labels. That regularity should make JML easier to learn and to use.

About the desugaring, I wondered what one would say about the value in a variable v that was declared local to a block, so what is the meaning of the following:

     {  labelE: Object v = new T();
        //@ assert \fresh(v, labelE);
     }

[davidcok]

It is not the variable that is fresh (or not), it is the value of that variable. In this case the value is that newly allocated T object. And as it is allocated since labelE, \fresh(v, labelE) is definitely true.

The semantics is slightly different with \old(v, labelE), as there we are asking to evaluate the expression 'v' in the state at labelE. As v is not in scope there, I consider \old(v, labelE) not well-defined. IN fact, if a different v were in scope, it would be that v (and its type) that would be evaluated.

[leavens]

I understand that the assertion in my example should be valid (pass). The question I have is: does the desugaring work in this case? That is does it make sense to translate the assertion into assert \fresh(v) && !\old(\fresh(v), labelE) ? In particular I worry about what \fresh(v) means at that point in the program; I suppose it is fine if it just means that the object that v refers to did not exist in the pre-state. But what does !\old(\fresh(v), labelE) make sense, since v is not in scope at the beginning of the statement labelled labelE?

[davidcok]

Sorry. I would say that !\old(\fresh(v), labelE) is ill-defined. One would have to write !\old(\fresh(\old(v,Here)), labelE)

[leavens]

So, for this proposal to make sense, some further work on the desugaring is needed to handle cases like this.

[mattulbrich]

In current JML \pre refers to the pre-state of the enclosing method and \old is the pre-state of the current contract (is context dependent).

According to §12.4.2:

An expression of the form \old(Expr) refers to the value that the expression Expr had in the pre-state of a method.

An expression of the form \pre(Expr) also refers to the value that the expression Expr had in the pre-state of a method. Expressions of this form may only be used in assertions that appear in the bodies of methods (i.e., in assert and assume statements, and in loop invariants and variant functions). That is, such expressions may not be used in specification cases, and hence may not appear in normal or exceptional postconditions, in history constraints, or in duration and working space clauses.

KeY currently implements this behaviour.

[davidcok]

The question of \pre \old and \before is taken up in #36.

As for \fresh, I think the consensus is that we allow \fresh with a label and that the semantics is that \fresh(e,L) is true iff the object that is the value of the expression e (evaluated in the current state) is fresh since the label L (rather than fresh since the pre-state of the enclosing contract, which is the default for L). Its desugaring, if we want one, requires using another concept, namely the allocation state of an object, and being able to speak of the allocation state of an object before it is, in Java, created.

This is similar but different than for \old, which evaluates its syntactic argument at the location of the given label. This is readily desugarable as a ghost initialization of a temporary variable to that expression at the location of the label. Nested differently-labels olds are more complex.

[leavens]

David @davidcok your consensus proposal seems good to me.

[mattulbrich]

Consensus:

As for \fresh, I think the consensus is that we allow \fresh with a label and that the semantics is that \fresh(e,L) is true iff the object that is the value of the expression e (evaluated in the current state) is fresh since the label L (rather than fresh since the pre-state of the enclosing contract, which is the default for L).

old and pre see #36.

[mattulbrich]

Addendum: We allow fresh with a label, but we do not require fresh to take a label.