Chromosome_false

function getScore(self: Ref, num: Int): Int function isNull(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 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 comp := 0 comp := comp + (getScore(o1, 1) == getScore(o2, 1) ? 0 : (getScore(o1, 1) > getScore(o2, 1) ? 1 : -1)) comp := comp + (getScore(o1, 2) == getScore(o2, 2) ? 0 : (getScore(o1, 2) > getScore(o2, 2) ? 1 : -1)) comp := comp + (getScore(o1, 3) == getScore(o2, 3) ? 0 : (getScore(o1, 3) > getScore(o2, 3) ? 1 : -1)) comp := comp + (getScore(o1, 5) == getScore(o2, 5) ? 0 : (getScore(o1, 5) > getScore(o2, 5) ? 1 : -1)) comp := comp + (getScore(o1, 7) == getScore(o2, 7) ? 0 : (getScore(o1, 7) > getScore(o2, 7) ? 1 : -1)) if (comp == 0) { returned := true res := 0 }else { if (comp > 0) { returned := true res := 1 }else{ returned := true res := -1 } } } assert returned }