PokerHand_false
PokerHand, incorrect version
function indexOf(self: Ref, pos: Int) : Int
function charAt(self: Ref, i: Int) : Int
function countOccurrencesOf(self: Ref, i : Int): Int
function lastIndexOf(self: Ref, i : Int): Int
define return(x) {
assert !returned
returned := true
res := x
}
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 ((indexOf(o1, 4) != -1) || (indexOf(o2, 4) != -1)) { // Four of a kind
if (indexOf(o1, 4) == indexOf(o2, 4)) {
var i1 : Int
i1 := 0
while(i1 <= 12 && !returned)
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(returned, 0) == rel(returned, 1))
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(i1, 0) == rel(i1, 1))
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> ((rel(returned, 0) && rel(returned, 1)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 1))))
{
if ((charAt(o1, i1) != 0) && (charAt(o1, i1) != 4) && (charAt(o2, i1) != 0) && (charAt(o2, i1) != 4)) {
return(0)
}elseif ((charAt(o1, i1) != 0) && (charAt(o1, i1) != 4)) {
return(-1)
}elseif ((charAt(o2, i1) != 0) && (charAt(o2, i1) != 4)) {
return(1)
}else{
i1 := i1 + 1
}
}
}
if (!returned) {
return(indexOf(o1, 4) - indexOf(o2, 4))
}
}else{
var tripleCount1 : Int
var tripleCount2 : Int
tripleCount1 := countOccurrencesOf(o1, 3);
tripleCount2 := countOccurrencesOf(o2, 3);
if ((tripleCount1 > 1) || ((tripleCount1 == 1) && (indexOf(o1, 2) != -1)) || (tripleCount2 > 1) || ((tripleCount2 == 1) && (indexOf(o2, 2) != -1))) { // Full house
var higherTriple: Int
higherTriple := lastIndexOf(o1, 3);
if (higherTriple == lastIndexOf(o2, 3)) {
var i2 : Int
i2 := 0
while(i2 <= 12 && !returned)
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(returned, 0) == rel(returned, 1))
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(i2, 0) == rel(i2, 1))
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> ((rel(returned, 0) && rel(returned, 1)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 1))))
{
if ((i2 != higherTriple) && (((charAt(o1, i2) == 2) || (charAt(o1, i2) == 3)) && ((charAt(o2, i2) == 2) || (charAt(o2, i2) == 3)))) {
return(0)
}elseif ((i2 != higherTriple) && ((charAt(o1, i2) == 2) || (charAt(o1, i2) == 3))) {
return(-1)
}elseif ((i2 != higherTriple) && ((charAt(o2, i2) == 2) || (charAt(o2, i2) == 3))) {
return(1)
}else{
i2 := i2 + 1
}
}
}
if (!returned) {
return(higherTriple - lastIndexOf(o2, 3));
}
}
if (!returned){
return(0)
}
}
assert returned
}