Closed wadoon closed 4 months ago
This version verifies the following program:
class A {
//@ ensures true;
void m() {
//@ ghost \bigint x = 0;
int i = 0;
while(i < 2) {
//@ ghost \bigint y = 1;
//@ set x = x + y;
i++;
}
//@ assert x == 0;
// but should be x == 2;
}
}
which is not correct at all. The problem is that in every loop iteration y becomes a different symbol. However, in x+y
the y remains always the original variable and is not updated to the respective instances. That is the reason why in assumptions and assertions the copy is kept and actually modified (breaking immutability).
Even simpler: The following can be proved:
void m() {
//@ ghost \bigint x = 0;
//@ set x = x + 1;
//@ assert x == 0;
}
The x in the set statement does not refer to the correct variable (neither when reading, nor when writing)
Then I would say, the simple does not work and we need to go back to the drawing board.
@unp1 Do you have insides into the mechanism of variable renaming? Is there a chance, to get around the ProgVarReplaceVisitor
completely? Why do we not book this information along a goal and/or a modality?
Everything is terrible. Current test program:
class Test {
//@ ghost int x;
int a;
//@ requires true; ensures x==a;
void foo() {
//@set x = 0;
a = 0;
//@set x = x + 1;
a = a + 1;
//@set x = x + 1;
a = a + 1;
//@set x = x + 1;
a = a + 1;
//@set x = x + 1;
a = a + 1;
//@set x = x + 1;
a = a + 1;
}
//@ ghost int rec;
int cer;
//@ requires a >= 0; ensures rec == cer; measured_by a;
int voo(int a) {
if (a == 0) {
//@ set rec = 0;
cer = 0;
return 0;
} else {
int r = voo(a - 1) + 1;
//@ set rec = r;
cer = r;
//@ assert r >=0;
return r;
}
}
}
There are only two possibilities:
@mattulbrich The mutable information of SetStatements
moved to SpecificationRepository
.
Hence, the AST is immutable again. If the change suits you, we need to adopt the JmlAssert
also.
The example above is proofable except for the faulty assert statement.
There are currently two construction sites:
PrettyPrinter
can not show the current expression, as it has no access to services or the spec repo.ProgVarReplacer
or IntroAtPreDefOps
.I would also now transform JMLAssert to SpecificationRepository
.
Added a new highlighting for JML statement:
The old highlighting was green, and was inherited from comments.
State not so bad:
Unit-Tests:
RAP:
Added a new highlighting for JML statement:
Would it perhaps make sense to deliberately deviate from JML like syntax here to avoid confusion on the user's side?
like //@ set a := 42
for instance or //@ set heap := heap[o.ghst := 42]
which is more faithful to the JavaDL side.
Perhaps even use //#
not //@
or something else to avoid confusion.
Attention: Patch coverage is 55.33333%
with 268 lines
in your changes are missing coverage. Please review.
Project coverage is 37.87%. Comparing base (
a5b90ec
) to head (45435fb
).
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Version of #3195 but with an immutable Java AST.
This PR implements JML set-statement in a non-Java-like fashion (no reduction to copy assignment) preserving the semantics of Java.
Translation of JML goes directly from JML to KeY terms lazily inside the built-in rule
SetStatementRule
.TODO
Type of pull request
Ensuring quality