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(o1, 1) && rel(o2, 0) == rel(o1, 2) && rel(o2, 2) == rel(o2, 1) && rel(res, 0) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 2))) 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(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 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) && 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 returned ==> res != 0 { comp := Int_compare(getScore(o1, i), getScore(o2, i)) if (comp != 0) { res := comp returned := true }else{ i := i + 1 } } if (!returned) { res := 0 returned := true } } assert returned }