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 34.61538% with 17 lines in your changes missing coverage. Please review.

Project coverage is 38.39%. Comparing base (284bb1e) to head (d616f00).
Report is 6 commits behind head on main.

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

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3571      +/-   ##
============================================
- Coverage     38.39%   38.39%   -0.01%     
- Complexity    17238    17239       +1     
============================================
  Files          2098     2098              
  Lines        127324   127346      +22     
  Branches      21442    21444       +2     
============================================
+ Hits          48886    48891       +5     
- Misses        72427    72441      +14     
- Partials       6011     6014       +3     

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

[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.