Names for JML entities

[wadoon]

STATE: This proposal is in an early stage, and tries to gather examples.

Motivation

Currently, we can not attach names to JML entities, like contracts or invariants.
Such names could improve the interaction between JML tools and the user, e.g.,
the tool could say which invariant (by name) is not provable, or the user could guide
the contract selection using the contract names.

Proposal

We extend JML body declaration, method contracts and loop contracts with the possibility to carry a name.

JML body declarations

class A {
   //@ public instance invariant INV_1 = true;
   //@ initially INIT = true;
   //@ accessible FOOTPRINT = o.f;
}

!! This syntax collides with the represents-clause.

JML field and method declarations already carries a names.

Contracts

Introduction of introducing the name clause. Note, the clause overwrites the name and is not cumulative when used in nested contracts. This clause was used in KeY a long time ago, but (somehow) the support was dropped.

/*@  public normal_behavior 
        name contract;
        ensures true; 
        requires true;
        {| 
           name contract;
           ensures a;
        |}    
*/