Closed mi-ki closed 3 months ago
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.
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
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.
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 ...
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).
Or take the method's assignable clause as a default like a number of other tools do. It is a good default.
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 ...
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.
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
.
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
.
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) usingassignable
.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
Ensuring quality
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.