Solution_false
Solution, incorrect version
function getValue(self: Ref) : Int
function solutionCost(self: Ref) : Int
function target() : 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
function abs(i: Int) : Int
{
i < 0 ? -i : i
}
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
var v1 : Int
var v2 : Int
v1 := getValue(o1)
v2 := getValue(o2);
if ((v1 == -1) && (v2 == -1)){
return(0)
}elseif (v1 == -1){
return(1)
}elseif (v2 == -1){
return(-1)
}elseif (v1 == v2){
return(sgn(solutionCost(o1) - solutionCost(o2)))
}
else {
return(sgn(abs(target()- v1) - abs(target() - v2)));
}
assert returned
}