public class StructuredAssertions { // s is non-null by default in JML private /*@ spec_public @*/ int[] s = new int[64]; /*@ @ requires (\exists int m; 0 <= m && m < s.length; s[m] == x); @ ensures s[\result] == x @ && (\forall int m; 0 <= m && m < \result; s[m] != x); @*/ public /*@ pure @*/ int findIndexPos(int x) { //@ maintaining (\exists int m; i <= m && m < s.length; s[m] == x); //@ maintaining (\forall int m; 0 <= m && m < i; s[m] != x); //@ decreasing s.length - i; for (int i = 0; i < s.length; i++) { if (s[i] == x) { return i; } } throw new IllegalArgumentException(); } //@ ensures \result == (\exists int m; 0 <= m && m < s.length; s[m] == x); public /*@ pure @*/ boolean ValuePresent (int x) { //@ maintaining (\forall int m; 0 <= m && m < i; s[m] != x); //@ decreasing s.length - i; for (int i = 0; i < s.length; i++) { if (s[i] == x) { return true; } } //@ assert (\forall int m; 0 <= m && m < s.length; s[m] != x); return false; } }