Formal Methods in Software Development

Exercise 6: JML Verification with OpenJML and KeY

Take from Exercise 5 the JML-annotated program functions replace, and subtract1. Perform for each of these

functions the tasks described below (you may use a single Java class file for all functions, but do

not include any test code or main functions in this file).

Annotate every loop in the function with an appropriate invariant (loop_invariant) and ter-

mination measure (decreases) and check these with escjava2 and openjmlesc. Please note

that escjava2 only checks whether the invariants hold after some iterations, i.e., only if an

invariant is too strong, it reports an error. On the other hand, openjmlesc inded tries to prove

the verification conditions generated from the invariants; if it reports an error, this may indicate

that an invariant is too weak. However, the openjmlesc prover is not complete; it may also fail

to prove a valid verification condition.

It is recommended to use multiple loop_invariant statements for each conjunct of the invariant;

then it is easier to determine which part of an invariant failed. In the case of a for loop, do not

forget to add the range condition for the loop variable to the invariant. If an array is modified, do

not forget to specify which part of the array has remained unchanged so far. Please use this function: /*@ public normal_behavior @ requires a != null; @ assignable a[*]; @ ensures (\forall int k; 0 <= k && k < a.length; @ \old(a[k]) == x ==> a[k] == y); @ ensures (\forall int k; 0 <= k && k < a.length; @ \old(a[k]) != x ==> a[k] == \old(a[k])); @ ensures esult == -1 ==> @ (\forall int k; 0 <= k && k < a.length; \old(a[k]) != x); @ ensures esult != -1 ==> @ 0 <= esult && esult < a.length && \old(a[ esult]) == x && @ (\forall int k; 0 <= k && k < esult; \old(a[k]) != x); @*/ public static int replace(char[] a, char x, char y) { int n = a.length; int result = -1; for (int i = n-1; i >= 0; i--) { if (a[i] == x) { a[i] = y; result = i; } } return result; }