After #3195, set and assert/assume statements are not handled inside Java anymore. Previous to this fix, the set statements were a regular copy assignment in Java. Therefore, classes were needed in the hierarchy of the Java AST to resemble JML expressions (e.g., empty set literal, ...). These classes are not needed anymore iff we push the migration further and transform declarations of ghost and model fields into set statements. The cases are
class A {
//@ ghost int x = (\num_of int y; 0<= y <= a.length; a[y]>0);
void foo() {
//@ ghost int x = (\sum ...);
}
}
TODO: Split ghost declaration into the declaration and the initialization part. The latter one can be handled via set statement. This requires a built-in rule. Better wait for a new JML framework.
Workaround until fix You do the split manually to have the full power of JML, e.g.,
void foo() { /*@ghost int x; set x = (\sum ...);*/ }
After #3195, set and assert/assume statements are not handled inside Java anymore. Previous to this fix, the set statements were a regular copy assignment in Java. Therefore, classes were needed in the hierarchy of the Java AST to resemble JML expressions (e.g., empty set literal, ...). These classes are not needed anymore iff we push the migration further and transform declarations of ghost and model fields into set statements. The cases are
TODO: Split ghost declaration into the declaration and the initialization part. The latter one can be handled via set statement. This requires a built-in rule. Better wait for a new JML framework.
Workaround until fix You do the split manually to have the full power of JML, e.g.,