method find(arr: array, e: int) returns (found: bool) ensures found ==> exists i: int :: 0 <= i < arr.Length && arr[i] == e ensures !found ==> forall i: int :: 0 <= i < arr.Length ==> arr[i] != e { found := false; var j := 0; //// <<<==== Is the invariant true here? while (j < arr.Length) invariant j <= arr.Length invariant found ==> exists i: int :: 0 <= i < arr.Length && arr[i] == e invariant !found ==> forall i: int :: 0 <= i < j ==> arr[i] != e { // Here, we know that j < arr.Length /// <=== Assume the invariant is true here, assume also that j < arr.Length if (arr[j] == e) { found := true; } ////// <==== Is the invariant true here? No! j := j + 1; ///// <==== Is the invariant once again true here? Yes! } // What do we know about j? j >= arr.Length and j <= arr.Length // arr[j] <<<=== This is a super bad array access! It will crash! // From invariant 1, it follows that, over here, j == arr.Length // From invariant 2, and the conclusion that j == arr.Length, // it follows that, over here, found ==> exists i: int :: 0 <= i < arr.Length && arr[i] == e // (Not coincidentally), this is the same as postcondition 1 }