Chromosome_true

function getScore(self: Ref, num: Int): Int function isNull(self: Ref): Int method Int_compare(o1: Int, o2: Int) returns (res: Int) ensures (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 1))) // P1 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 isNull(o1) != 0 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 res := 0 if (isNull(o2) == 0) { returned := true res := 1 } if (!returned) { var comp : Int var i : Int comp := 0 i := 0 while (i < 5 && !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(i, 0) == rel(i, 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)))) { comp := Int_compare(getScore(o1, i), getScore(o2, i)) if (comp != 0) { res := comp returned := true } i := i + 1 } if (!returned) { res := 0 returned := true } } assert returned }