Exploiting JML Names in the Proof Tree

[wadoon]

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:

  //@ 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:

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 ❗

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:

[wadoon]

Still struggling about the differences in the proofs.

Added a GUI for finding differences in proof trees and sequents.

[WolframPfeifer]

For me, the generation of name labels seems to work only partially:

class Labels {
    int f = 7; 
    //@ invariant inv1: f == 7;
    /*@ requires pre1: x == 5;
      @ ensures post1: \result == 42;
      @ ensures post2: \result == \lbl(prod, 6 * 7);
      @*/
    int m(int x) {
        return 42;
    }
}

Only the formula with lbl got a label as expected. Am I doing something wrong here?

[mattulbrich]

I mark this "Work in progress" since a number of checks fail. Please undo if/when ready to review.

[wadoon]

This is a typical example that KeY development is dysfunctional.

It was green, and nobody reviewed it, after repeatedly merging the main branch into it, it became red.

I do not see any reason to invest further time into it, only to see the branch rot away until the next review.

[WolframPfeifer]

This is a typical example that KeY development is dysfunctional.

It was green, and nobody reviewed it, after repeatedly merging the main branch into it, it became red.

I do not see any reason to invest further time into it, only to see the branch rot away until the next review.

I reviewed it a long time ago, had some fundamental questions, remarks, and pointed out some bugs (#3022 (review)). In my opinion, this is my job as a reviewer. Until now, I did not get any answer to those (see #3022 (review) and #3022 (comment)), so I do not consider it my job to do another review until my points are answered/resolved.

I think that the job of the developer is to provide a working, tested and high quality PR (at least with a clear concept, a description with a list of the changes it contains, good documentation, passing CI tests). Only having "green tests" is not sufficient ...

And if my questions have been resolved in the meantime, I would expect at least a comment answering them, not just a re-request of a review ...