Introducing some structure for model method bodies

[mattulbrich]

Intended Change

This is a new feature request by users that wanted to use model methods.

The PR introduces method bodies that allow some statements. It is limited to

• introducing local variables and variable assignment in method bodies.
• introducing if-statements
• return statements (as they have been there before)

This is still rather limited but allows you to structure your code already quite a bit.
The restrictions are:

• Every if-branch-path must eventually contain a return statement (no phi-nodes)
• Variables must be defined with var (due to a restriction in the lexer/parser)

The only thing that needs to be done is then to interpret these structures into a term.

My running example is the following which explains itself:

final class A {

    /*@ pure */
    int f(int x) {
        return 40-x;
    }
    
    /*@ model int maxF(int x, int y) {
      @   var x2 = f(x);
      @   var y2 = f(y);
      @   if(x2 > y2)
      @      return x2;
      @   else {
      @      return y2;
      @   }
      @ }
      @*/

    /*@ normal_behaviour
      @  ensures maxF(25, 30) == 15;
      @*/
    void test() { }

}

Plan

• Implement the feature
• Make sure we have consensus on wanting this

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• Other: Changes to JML lexer and parser

Ensuring quality

• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[codecov]

Codecov Report

Attention: Patch coverage is 23.07692% with 30 lines in your changes missing coverage. Please review.

Project coverage is 39.58%. Comparing base (db46d41) to head (d2fe29f).
Report is 23 commits behind head on main.

Files with missing lines	Patch %	Lines
...java/de/uka/ilkd/key/speclang/njml/Translator.java	21.05%	27 Missing and 3 partials ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3571      +/-   ##
============================================
+ Coverage     39.54%   39.58%   +0.03%     
- Complexity    17753    17778      +25     
============================================
  Files          2103     2103              
  Lines        127774   127810      +36     
  Branches      21500    21504       +4     
============================================
+ Hits          50527    50590      +63     
+ Misses        71050    71026      -24     
+ Partials       6197     6194       -3     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[wadoon]

My questions would also be:

• Why keep it limited to if statements? In jmlparser all Java/JML-constructs are allowed.
• Does pure require termination?

Maybe we should add a jmlFrame : { } (in contrast to method-frame: {}) to allow more statements, and also have a different execution semantics.

[mattulbrich]

My questions would also be:
Why keep it limited to if statements? In jmlparser all Java/JML-constructs are allowed.

Because thus jml model method bodies can remain purely logical expressions and their definition can be directly expanded into the sequent. That is a fundamental asset of model methods as they are implemented in KeY (like related constructs in other verification frameworks). Dealing with loops in particular would make this impossible.

This was driven by trying to relax notation while keeping the verification-system power of the type definitions.

How does the JavaDL-definition axiom or taclet for model methods look like in jmlparser?

Does pure require termination?

I think actually, it does. In KeY, however, the expansion mechanism for non-model methods, is conservative and uses [] box-semantics to be on the safe side.

Maybe we should add a jmlFrame : { } (in contrast to method-frame: {}) to allow more statements, and also have a different execution semantics.

I would refrain from putting jml model methods into modalities, It's their power to define functions directly.

I would be happy to intrdoduce ghost methods that can use any code. They do not even need to be pure.
ghost loops/ifs in regular methods would also be really cool.

[mattulbrich]

The implementation renders the local variables into "let expressions" which are {\subst ...} constructs in KeY.
Currently, these are exposed onto the sequent when proving model methods:

Is it bad that subst makes it to the surface here? Could also be easily avoided by expanding them during translation. ... On the other hand: It renders the user-defined structure into the logic. There are fully automatic (OSS-)taclets in place that expand the substitutions.

[wadoon]

Is it bad that subst makes it to the surface here?

No. Trust the sound rules in KeY.

IMHO, it is strange that you do not use updates here instead of substitutions.

[mattulbrich]

IMHO, it is strange that you do not use updates here instead of substitutions.

Well observed. The reason behind this that updates operate only on global program variables whereas substitutions operate on logical variables which are not part of a global namespace. It would not be advisable to clutter the program varoable namespace with symbols needed for temporary local value assignment.

[mattulbrich]

The feature has been mentioned in the keydocs (although they are not very structured)

The Boyer Moore example has been adapted to the new syntax capabilities.

[wadoon]

Why am I not allowed to have variable decls inside if-then-else constructs? Flow analysis too hard?