PokerHand_true
PokerHand, correct 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(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
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 i1 >= 0 && i1 <= 13
invariant (forall j : Int :: j >= 0 && j < i1 ==> (!((charAt(o1, j) != 0) && (charAt(o1, j) != 4)) && !((charAt(o2, j) != 0) && (charAt(o2, j) != 4))))
invariant returned && res > 0 ==> i1 <= 12 && ((charAt(o2, i1) != 0) && (charAt(o2, i1) != 4)) && !((charAt(o1, i1) != 0) && (charAt(o1, i1) != 4))
invariant returned && res < 0 ==> i1 <= 12 && !((charAt(o2, i1) != 0) && (charAt(o2, i1) != 4)) && ((charAt(o1, i1) != 0) && (charAt(o1, i1) != 4))
invariant returned && res == 0 ==> i1 <= 12 && ((charAt(o2, i1) != 0) && (charAt(o2, i1) != 4)) && ((charAt(o1, i1) != 0) && (charAt(o1, i1) != 4))
{
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))) { // c1 Full house
if ((tripleCount2 > 1) || ((tripleCount2 == 1) && (indexOf(o2, 2) != -1))) { // c2 Full house too
var higherTriple : Int
higherTriple := lastIndexOf(o1, 3);
if (higherTriple == lastIndexOf(o2, 3)) {
var i2 : Int
i2 :=0;
while(i2 <= 12 && !returned)
invariant i2 >= 0 && i2 <= 13
invariant (forall j : Int :: j >= 0 && j < i2 ==> (!((j != higherTriple) && ((charAt(o2, j) == 2) || (charAt(o2, j) == 3))) && !((j != higherTriple) && ((charAt(o1, j) == 2) || (charAt(o1, j) == 3)))))
invariant returned && res > 0 ==> i2 <= 12 && ((i2 != higherTriple) && ((charAt(o2, i2) == 2) || (charAt(o2, i2) == 3))) && !((i2 != higherTriple) && ((charAt(o1, i2) == 2) || (charAt(o1, i2) == 3)))
invariant returned && res < 0 ==> i2 <= 12 && !((i2 != higherTriple) && ((charAt(o2, i2) == 2) || (charAt(o2, i2) == 3))) && ((i2 != higherTriple) && ((charAt(o1, i2) == 2) || (charAt(o1, i2) == 3)))
invariant returned && res == 0 ==> i2 <= 12 && ((i2 != higherTriple) && ((charAt(o2, i2) == 2) || (charAt(o2, i2) == 3))) && ((i2 != higherTriple) && ((charAt(o1, i2) == 2) || (charAt(o1, i2) == 3)))
{
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))) { // only c1 Full house
return(-1)
}elseif ((i2 != higherTriple) && ((charAt(o2, i2) == 2) || (charAt(o2, i2) == 3))) { // only c2 Full house
return(1)
}else{
// missing in descartes
i2 := i2 + 1
}
}
}
if (!returned) {
return(higherTriple - lastIndexOf(o2, 3));
}
}
if (!returned) {
return(1)
}
}else{
if ((tripleCount2 > 1) || ((tripleCount2 == 1) && (indexOf(o2, 2) != -1))) {
return(-1)
}else{
return(0)
}
}
}
assert returned
}