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

• [x] Better branch names for origin label
• [x] Test function for the introduction of abbreviations on sequent based on name label.
• [x] Discuss impact on proof scripts. Extend proofs scripts with abbreviation variable? @post_abc?
• [x] 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 :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:

[wadoon]

@mattulbrich @unp1 @WolframPfeifer @jwiesler @flo2702

Help required

This PR is feature complete, but some proofs do not close anymore. It seems that term label indeed affect the calculus.

You can see this on the SumAndMax example. The example given in the "Example Chooser" is still provable, whereas key.ui/examples/dynamicBranchLabels/SumAndMax is not provable. The first difference in the proof tree I noted is a different cut formula.

Does anyone is deeper in the topic or can look at it?

[wadoon]

Does anyone is deeper in the topic or can look at it?

@flo2702 gave a tip: TermLabel#isProofRelevant defines whether a term label should be considered by the strategy.

It helped a little bit, but the SumAndMax does not close.

[wadoon]

Still struggling about the differences in the proofs.

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

[wadoon]

SumAndMax runs. It was a missing setting.

Proof tree look as follows:

@WolframPfeifer

Is it possible to achieve to make cut branch names "If x_5 is TRUE" more useful? Could we not add a term label (dynamical added) to x_5 that origin is "if-cond is line X"? And make a term label "If if-cond:X (x_5) is TRUE"?

[github-actions[bot]]

Thank you for your contribution.

The test artifacts are available on Artiweb. The newest artifact is here.

[jwiesler]

Couldn't we make branch labels just any complex type instead of string and let the GUI decide what to display? This would allow more control over what is displayed, how, and where. This type could contain origin, the cut term in this case and more. As a fallback we could always construct a string from this representation to be used in e.g. proof scripts if needed.

An example that comes to my mind instantly is pretty printing branch labels in the tooltip.

[wadoon]

Couldn't we make branch labels just any complex type instead of string and let the GUI decide what to display?

Possible. But I see negative impact on computing time and memory, and also not the use case of different renderers in the UI.

In principle, we can today recompute all labels in the current situation, also with the branching name label.

[WolframPfeifer]

After some debugging, I think I found the problem. The syntax clashes with the syntax of dependency contracts for model fields/methods (see accessible clauses below):

class MyClass {
    int attr;
    int attr2;

    //@ model \locset footprint;
    //@ represents footprint = this.*;
    //@ accessible footprint: footprint;

    //@ invariant attr2 != 0;
    //@ accessible \inv: footprint;
   
   ...
}

[codecov[bot]]

Codecov Report

Attention: Patch coverage is 69.55017% with 88 lines in your changes missing coverage. Please review.

Project coverage is 38.00%. Comparing base (1b48b9e) to head (ca27737). Report is 92 commits behind head on main.

:exclamation: Current head ca27737 differs from pull request most recent head 93c20fc

Please upload reports for the commit 93c20fc to get more accurate results.

Files	Patch %	Lines
...java/de/uka/ilkd/key/settings/GeneralSettings.java	40.35%	34 Missing :warning:
...ule/tacletbuilder/branchlabel/MiniLabelParser.java	78.72%	5 Missing and 5 partials :warning:
...eclang/jml/pretranslation/TextualJMLConstruct.java	42.85%	4 Missing and 4 partials :warning:
...eclang/jml/pretranslation/TextualJMLInitially.java	0.00%	5 Missing :warning:
...kd/key/speclang/njml/LabeledParserRuleContext.java	70.58%	3 Missing and 2 partials :warning:
...ava/de/uka/ilkd/key/logic/label/SpecNameLabel.java	71.42%	3 Missing and 1 partial :warning:
...java/de/uka/ilkd/key/speclang/njml/Translator.java	0.00%	4 Missing :warning:
...ey/rule/tacletbuilder/branchlabel/NameLabelOf.java	88.00%	3 Missing :warning:
...peclang/jml/pretranslation/TextualJMLClassInv.java	66.66%	2 Missing and 1 partial :warning:
...main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java	75.00%	1 Missing and 2 partials :warning:
... and 8 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3022      +/-   ##
============================================
- Coverage     38.03%   38.00%   -0.03%     
- Complexity    17089    17090       +1     
============================================
  Files          2099     2066      -33     
  Lines        127274   126506     -768     
  Branches      21386    21330      -56     
============================================
- Hits          48409    48080     -329     
+ Misses        72892    72527     -365     
+ Partials       5973     5899      -74     

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[mattulbrich]

Should that perhaps be made WIP since there are still open todos?

[wadoon]

Should that perhaps be made WIP since there are still open todos?

No. It is reviewable.

[wadoon]

Time to finish this. Tests are green. Spotless should also be happy.

[wadoon]

@WolframPfeifer it is green. Auto-merge error.

[WolframPfeifer]

I already did a review recently and have not yet received any answers to my questions from back then. I am still missing a clear concept in this PR, it seems really arbitrary at some points (questions 1 and 2 in the list). The most important point is that I think that there are serious problems with using the term labels (point 4). However, the documentation is better now, thanks.

[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 (https://github.com/KeYProject/key/pull/3022#pullrequestreview-1982375448). In my opinion, this is my job as a reviewer. Until now, I did not get any answer to those (see https://github.com/KeYProject/key/pull/3022#pullrequestreview-1676265076 and https://github.com/KeYProject/key/pull/3022#issuecomment-1821359860), 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 ...