Chromosome_false
Chromosome, incorrect version
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(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
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
}