ArrayInt_false

function get(self: Ref, pos: Int): Int function length(self: Ref): Int 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(o2, 1) && rel(o2, 0) == rel(o1, 1) ensures (sgn(rel(res, 0)) == -sgn(rel(res, 1))) // P1 { 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 (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(returned, 0) == rel(returned, 1)) invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(index, 0) == rel(index, 1)) invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> ((rel(returned, 0) && rel(returned, 1)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 1)))) { 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 }