CollItem_true
CollItem, correct version
function getCardSet(self: Ref): Int
function getCardRarity(self: Ref): Int
function getCardId(self: Ref): Int
function cardType(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 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
if (o1 == o2){
res := 0
returned := true
}
if (!returned && getCardSet(o1) > getCardSet(o2)) {
res := 1
returned := true
}
if (!returned && getCardSet(o1) < getCardSet(o2)) {
res := -1
returned := true
}
if (!returned && getCardRarity(o1) < getCardRarity(o2)) {
res := 1
returned := true
}
if (!returned && getCardRarity(o1) > getCardRarity(o2)) {
res := -1
returned := true
}
if (!returned && getCardId(o1) > getCardId(o2)) {
res := 1
returned := true
}
if (!returned && getCardId(o1) < getCardId(o2)) {
res := -1
returned := true
}
if (!returned) {
res := cardType(o1) - cardType(o2)
returned := true
}
assert returned
}