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(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
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
}