Exploiting JML Names in the Proof Tree #3022

This PR adds the newly introduced JML names for entities to KeY. Such labels are exploited inside the KeY's proof tree as branching labels. And may later become accessible in proof scripts.

This MR brings following changes:

• JML entities have names: java //@ invariant NAME: true; //@ ensures<h1> NAME: true; //@ behavior NAME: requires NAME1: true;

• lbl function is supported, e.g., \lbl(NAME, x != y)

• A new term label name(XXX) is added, where "XXX" holds the name given in the JML specification.

• Terms that are created by the JMLParser/Translator receive a this term label if the entity has a name or a \lbl was given.

• Change to the KeY parser: Goal templates can have computed labels.

Currently, the label of a goal can be a schema variable or static string. With this MR you are allowed to define labels which are computed by a Java interface BranchNamingFunction. A taclet exploits this in the following way:

andRight { \find (==> b & c) "\nameLabelOf(b)":\replacewith(==> b); "\nameLabelOf(c)":\replacewith(==> c) \heuristics(beta) };

New branching naming functions can be added by an interface. The \nameLabelOf tries to find a f«name(X)» term label, and returns X. It fallbacks to the origin term label and then to the toString representation.

TODO

• [ ] Better branch names for origin label
• [ ] Test function for the introduction of abbreviations on sequent based on name label.
• [ ] Discuss impact on proof scripts. Extend proofs scripts with abbreviation variable? @post_abc?
• [ ] andRightX and orLeftX per Built-In rule?

KeY example (working)

\sorts { s; } \predicates { p; q; } \problem { (p<<name("A")>> -> q<<name("B")>>) -> !q<<name("C")>> -> !p<<name("D")>> }

New rules andRightX (for $x \in 3..6$) allows a more comprehensible proof split.

JML

Consider following examples:

```java class Test { //@ public invariant MY_SUPER_INVARIANT: CONST == 42;

public final int CONST = 42;
/*@
requires Z: this != null;
ensures A: \result == 42;
ensures B: \result >= 0;
ensures C: \result != 0;
*/
public int foo() {return CONST;}

} ```

This results into the following proof tree. At places where no name label is available we ask the origin label for a string representation. The origin label needs further improvement e.g., line numbers :exclamation:

Sum And Max

``` class SumAndMax {

int sum;
int max;

/*@ normal_behaviour
  @   requires R1: (\forall int i; 0 <= i && i < a.length; 0 <= a[i]);
  @   assignable sum, max;
  @   ensures E1: (\forall int i; 0 <= i && i < a.length; a[i] <= max);
  @   ensures E2: (a.length > 0
  @           ==> (\exists int i; 0 <= i && i < a.length; max == a[i]));
  @   ensures E3: sum == (\sum int i; 0 <= i && i < a.length; a[i]);
  @   ensures E4: sum <= a.length * max;
  @*/
void sumAndMax(int[] a) {
    sum = 0;
    max = 0;
    int k = 0;

    /*@ loop_invariant I1: 0 <= k && k <= a.length;
      @ loop_invariant I2: (\forall int i; 0 <= i && i < k; a[i] <= max);
      @ loop_invariant I3: (k == 0 ==> max == 0);
      @ loop_invariant I4: (k > 0 ==> (\exists int i; 0 <= i && i < k; max == a[i]));
      @ loop_invariant I5: sum == (\sum int i; 0 <= i && i< k; a[i]);
      @ loop_invariant I6: sum <= k * max;
      @
      @  assignable sum, max;
      @  decreases a.length - k;
      @*/
    while(k < a.length) {
        if(max < a[k]) {
            max = a[k];
        }
        sum += a[k];
        k++;
    }
}

} ```

Introduction of Abbreviations for Named Terms

Menu: Proof-> Introduce abbreviation for named formulas

Before:

After actions is applied: