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 ensures (rel(o1, 0) == rel(o2, 2) && rel(o2, 0) == rel(o1, 2)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 2))) // P1 ensures (rel(o1, 2) == rel(o2, 1) && rel(o2, 2) == rel(o1, 1)) ==> (sgn(rel(res, 2)) == -sgn(rel(res, 1))) // P1 ensures (rel(o1, 0) == rel(o1, 1) && rel(o2, 0) == rel(o2, 1)) ==> (rel(res, 0) == rel(res, 1)) // deterministic ensures (rel(o1, 0) == rel(o1, 2) && rel(o2, 0) == rel(o2, 2)) ==> (rel(res, 0) == rel(res, 2)) // deterministic ensures (rel(o1, 2) == rel(o1, 1) && rel(o2, 2) == rel(o2, 1)) ==> (rel(res, 2) == rel(res, 1)) // deterministic ensures ((rel(res, 0) > 0) && rel(res, 1) > 0 && rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)) ==> (rel(res, 2) > 0) // P2 ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 0) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 2))) ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 1) == 0) ==> (sgn(rel(res, 0)) == sgn(rel(res, 2))) ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 2) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 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 isNull(o1) != 0 requires rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) ensures ((rel(res, 0) > 0) && rel(res, 1) > 0) ==> (rel(res, 2) > 0) // P2 { 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(returned, 0) && !rel(returned, 1)) ==> (rel(i, 0) == rel(i, 1)) invariant (!rel(returned, 2) && !rel(returned, 1)) ==> (rel(i, 2) == rel(i, 1)) invariant (!rel(returned, 0) && !rel(returned, 2)) ==> (rel(i, 0) == rel(i, 2)) invariant (!rel(returned, 0) && !rel(returned, 1)) ==> (!rel(returned, 2)) invariant (!rel(returned, 2) && !rel(returned, 1)) ==> (!rel(returned, 0)) invariant (!rel(returned, 0) && !rel(returned, 2)) ==> (!rel(returned, 1)) invariant (!rel(returned, 0) && rel(returned, 1)) ==> (rel(returned, 2) && sgn(rel(res, 1)) == sgn(rel(res, 2))) invariant (!rel(returned, 0) && rel(returned, 2)) ==> (rel(returned, 1) && sgn(rel(res, 2)) == sgn(rel(res, 1))) invariant (!rel(returned, 1) && rel(returned, 0)) ==> (rel(returned, 2) && sgn(rel(res, 0)) == sgn(rel(res, 2))) invariant (!rel(returned, 1) && rel(returned, 2)) ==> (rel(returned, 0) && sgn(rel(res, 2)) == sgn(rel(res, 0))) invariant ((rel(returned, 0) && rel(res, 0) > 0) && rel(returned, 1) && rel(res, 1) > 0) ==> (rel(returned, 2) && rel(res, 2) > 0) { 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 }