ArrayInt_false

function get(self: Ref, pos: Int): Int function length(self: Ref): Int ensures result >= 0 function sgn(i: Int) : Int ensures i > 0 ==> result == 1 ensures i == 0 ==> result == 0 ensures i < 0 ==> result == -1 method compare(o1: Ref, o2: Ref) returns (res: Int) requires rel(o1, 0) == rel(o1, 1) && rel(o2, 0) == rel(o1, 2) && rel(o2, 2) == rel(o2, 1) ensures (rel(res, 0) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 2))) // P3 { var returned : Bool returned := false var index : Int var aentry : Int var bentry : Int index := 0 while (index < length(o1) && index < length(o2) && !returned) invariant index >= 0 && index <= length(o1) && index <= length(o2) invariant returned ==> res != 0 invariant (forall j : Int :: j >= 0 && j < index ==> (get(o1, j) == get(o2, j))) invariant returned && res > 0 ==> index < length(o1) && index < length(o2) && get(o1, index) > get(o2, index) invariant returned && res < 0 ==> index < length(o1) && index < length(o2) && get(o1, index) < get(o2, index) { aentry := get(o1, index) bentry := get(o2, index) if (aentry < bentry) { returned := true res := -1 } if (!returned && aentry > bentry) { returned := true res := 1 } if (!returned) { index := index + 1 } } if (!returned) { res := 0 returned := true } assert returned }