Node_false
Node, incorrect version
function getID(self: Ref) : Int
function containsKey(self: Ref, id: Int) : Bool
function get(self: Ref, id: 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(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(containsKey(o1, getID(o1)) && containsKey(o2, getID(o2))){
var order1 : Int
order1 := get(o1, getID(o1))
var order2 : Int
order2 := get(o2, getID(o2))
if(order1 < order2){
return(-1)
}else{
if(order1 > order2){
return(1)
}else{
return(0)
}
}
}
if (!returned) {
return(0)
}
assert returned
}