class StructuredAssertions { var S: seq; function InIndexRange(j: int): bool reads this; { 0 <= j && j < |S| } method Find_Index_Pos(x: int) returns (pos: int) requires (exists j :: InIndexRange(j) && S[j] == x); ensures InIndexRange(pos) && S[pos] == x; ensures (forall j :: InIndexRange(j) && j < pos ==> S[j] != x); { pos := 0; while (true) invariant InIndexRange(pos); invariant (forall j :: InIndexRange(j) && j < pos ==> S[j] != x); decreases |S| - pos; { if (S[pos] == x) { return; } pos := pos + 1; } } method Value_Present(x: int) returns (p: bool) ensures p <==> (exists j :: InIndexRange(j) && S[j] == x); { var i := 0; while (i < |S|) invariant 0 <= i && i <= |S|; invariant (forall j :: InIndexRange(j) && j < i ==> S[j] != x); decreases |S| - i; { if (S[i] == x) { p := true; return; } i := i + 1; } p := false; } }