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)
• [x] New feature (non-breaking change which adds functionality)
• [ ] Breaking change (fix or feature that would cause existing functionality to change)
• [x] 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.
• [x] 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[bot]]

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.

:exclamation: 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 :warning:
...de/uka/ilkd/key/speclang/WellDefinednessCheck.java	4.76%	40 Missing :warning:
...ava/de/uka/ilkd/key/speclang/LoopContractImpl.java	0.00%	28 Missing :warning:
.../key/speclang/FunctionalOperationContractImpl.java	50.00%	21 Missing and 1 partial :warning:
...d/key/speclang/jml/translation/JMLSpecFactory.java	52.17%	5 Missing and 17 partials :warning:
...e/uka/ilkd/key/rule/AbstractLoopInvariantRule.java	0.00%	20 Missing :warning:
...e/uka/ilkd/key/proof/init/AbstractOperationPO.java	40.00%	15 Missing :warning:
...in/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java	45.45%	10 Missing and 2 partials :warning:
...ava/de/uka/ilkd/key/rule/ObserverToUpdateRule.java	0.00%	11 Missing :warning:
...va/de/uka/ilkd/key/speclang/BlockContractImpl.java	15.38%	11 Missing :warning:
... 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     

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: 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]

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.

[mattulbrich]

While the title says this PR introduces new alias names, it seems that it changes the default keyword. I am not sure we all agree on doing that ...

[mi-ki]

While the title says this PR introduces new alias names, it seems that it changes the default keyword. I am not sure we all agree on doing that ...

Thanks for your feedback! Can you please say what you mean by default keyword? I did not implement any automatic specification generation/inference or similar, and this PR is really only about aliases.

What you may be referring to, is how some variables in KeY's Java code are named. Here, I tried to make the naming more consistent and honest (and hence: less misleading) about what KeY actually implements (see, e.g., also https://dafny.org/latest/DafnyRef/DafnyRef#sec-modifies-clause) but this does not affect the user, I believe.

[mattulbrich]

It seemed to me that you renamed a few things from "assignable" to "modifiable", also in error messages. That led me to the conclusion that "modifiable" is the new default keyword. Btw. in the old days in KeY (and currently in Danfy) the keyword was modifies.

[mi-ki]

Thanks for spotting that, I reverted my changes in the two respective error messages now and added explanatory comments. Yep, in the link that I had provided, Dafny also compares to KeY's semantics as well as ACSL(++) and Ada/SPARK. From their description, it seems that Ada/SPARK’s dataflow contracts actually have a semantics of assignable.