Introduce JML aliases of frame conditions for better tool compatibility

[mi-ki]

This pull request allows handling various aliases for frame conditions within method/block/loop contracts and loop specifications. These aliases cover the ones which are used in various other verification tools with contracts for Java-like programs, e.g., Krakatoa, OpenJML, Dafny, ACSL++, or CorC.

In particular, the following aliases are henceforth supported for frame conditions in method, block, and loop contracts as well as loop specifications:

assignable, assigns, assigning, modifiable, modifies, modifying, writable, writes, writing.

Upon usage of the italic versions, we throw a warning in order to distinguish expected semantics, e.g., from runtime verification, as KeY does static analysis, but (other than potentially seeing a warning) these versions are supported in the same way as the other aliases.

For loop specifications, we also support the respective aliases with the prefix loop_.

During discussions on this pull request, it was noted that the semantics implemented within KeY might be better captured by modifiable, but for legacy reasons, we do not move away from (also) using assignable.

Related Issue

This pull request addresses #3362.

Intended Change

This pull request introduces the aliases for frame conditions which are shown above. Thereby, it increases compatibility with further tools using JML, JML variants, or JML-alikes, such as Krakatoa, OpenJML, Dafny, or ACSL++.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behavior should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other:

Ensuring quality

• I made sure that introduced/changed code is well documented (Javadoc and inline comments).
• 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.
• I have tested the feature as follows: Checked it for the example from the referenced issue.
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

Some of the changes are results from work at the HacKeYthon together with @unp1.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[codecov]

Codecov Report

Attention: Patch coverage is 44.74018% with 436 lines in your changes missing coverage. Please review.

Project coverage is 37.87%. Comparing base (345c9c6) to head (0aced40).
Report is 1 commits behind head on main.

❗ Current head 0aced40 differs from pull request most recent head b46cd7a

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

Files	Patch %	Lines
...kd/key/speclang/AbstractAuxiliaryContractImpl.java	34.37%	39 Missing and 3 partials ⚠️
...de/uka/ilkd/key/speclang/WellDefinednessCheck.java	4.76%	40 Missing ⚠️
...ava/de/uka/ilkd/key/speclang/LoopContractImpl.java	0.00%	28 Missing ⚠️
.../key/speclang/FunctionalOperationContractImpl.java	50.00%	21 Missing and 1 partial ⚠️
...d/key/speclang/jml/translation/JMLSpecFactory.java	52.17%	5 Missing and 17 partials ⚠️
...e/uka/ilkd/key/rule/AbstractLoopInvariantRule.java	0.00%	20 Missing ⚠️
...e/uka/ilkd/key/proof/init/AbstractOperationPO.java	40.00%	15 Missing ⚠️
...in/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java	45.45%	10 Missing and 2 partials ⚠️
...ava/de/uka/ilkd/key/rule/ObserverToUpdateRule.java	0.00%	11 Missing ⚠️
...va/de/uka/ilkd/key/speclang/BlockContractImpl.java	15.38%	11 Missing ⚠️
... and 57 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3365      +/-   ##
============================================
- Coverage     38.03%   37.87%   -0.16%     
- Complexity    17084    17085       +1     
============================================
  Files          2099     2086      -13     
  Lines        127194   127537     +343     
  Branches      21368    21475     +107     
============================================
- Hits          48375    48305      -70     
- Misses        72856    73309     +453     
+ Partials       5963     5923      -40     

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

[fab918]

I tried the following example:

    /*@ requires array != null && array.length > 0;
      @ ensures \result == (\sum int i; 0 <= i && i < array.length; array[i]);
      @ assignable \nothing;
      @*/
    public static int sum(int[] array) {
        int total = 0;
        
        //@ maintaining 0 <= i && i <= array.length;
        //@ maintaining total == (\sum int j; 0 <= j && j < i; array[j]);
        //@ decreases array.length - i;
        //@ loop_writes \nothing;
        for (int i = 0; i < array.length; i++) {
            total += array[i];
        }
        return total;
    }

In the KeY-2.12.2 (2023-11-10) release: this file can't be loaded:

de.uka.ilkd.key.speclang.translation.SLTranslationException: Could not translate JML specification. You have either tried to use an unsupported keyword (loop_writes) or a JML field declaration without a ghost or model modifier.  Caused by: java.lang.RuntimeException: de.uka.ilkd.key.speclang.translation.SLTranslationException: Could not translate JML specification. You have either tried to use an unsupported keyword (loop_writes) or a JML field declaration without a ghost or model modifier.

In the PR: the file can be loaded and you are correctly returned to the main interface.

However, the proof doesn't work, it looks like the annotation is just skipped. Besides, it's not in bold as you can see in the screenshot, so I guess you need to add something else for the alias to work.

[WolframPfeifer]

First of all, I think it is a good idea to be able to parse these keywords. However, I am not sure if we want to allow these as aliases (at least not without a warning). Intuitively, modified (is changed by the loop/method) and modifiable (may be changed) have slightly different semantics. Since KeY uses the latter, I am not sure if it is a good idea to allow these aliases.

The original JML reference manual is old and outdated; as far as I can see, there is no framing clause for loops at all. The new one is still unfinished (and will take a while), I could not find a conclusion on the allowed keywords for framing clauses (neither in the PDF nor in the discussion on GitHub). I think that we should come up with our own consistent concept here. My suggestion would be:

1. framing clauses for methods:
   • assignable, modifiable, writable
   • assigns, modifies, writes (*)
   • I would not support assigning etc.
2. framing clauses for loops:
   • all of the above
   • all of the above with additional loop_ prefixes (although personally I prefer the variants without prefix)

For (*) and the variants with prefix, there should be a warning, since KeY uses modifiable/assignable semantics. Actually, one could argue that there is even a subtle difference between those two (as far as I remember also mentioned in the KeY book in a gray box). However, that would probably go too far ...

Btw.: The clauses still need to be translated to logic, I think this has to be done somewhere in JMLSpecFactory/TextualJMLSpecCase.

[WolframPfeifer]

Btw.: The support of syntax highlighting in the SourceView panel (screenshot above) is completely independent, as it is done by a handwritten highlighter and has its own list of supported keywords. Not ideal, but very difficult to do better ...

[WolframPfeifer]

Since the reason for the failed proof attempt in #3362 was the missing framing clause, it would probably make sense to show a warning if no framing clause is present (default is assignable \everything, which is rarely what you want).

[mattulbrich]

Or take the method's assignable clause as a default like a number of other tools do. It is a good default.

[WolframPfeifer]

Thanks, apart from some minor comments, I think that the changes are good. One thing I noticed though: Could it be the case that the performance of the parser dropped? It seems that loading the examples takes longer now (I did not measure, just some impression).

In addition, I put the PR onto the discussion list for our developer meetings (KaKeY), since I am not sure if moving towards "modifiable" is a good idea after having "assignable" basically as default for such a long time (even if it is only in code for now). Maybe we should discuss if everybody is ok with that.

[WolframPfeifer]

Thanks, I think having support for more framing keywords (also with the warning about possibly unintended semantics) is beneficial.

Also, thanks for removing ambiguities from the variable names, where mod stood for either modifier or modality or modifiable ;-)