Time_false
Time, incorrect version
function ora(self: Ref) : Int
function volume_totale(self: Ref) : 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 Int_compare(o1: Int, o2: Int) returns (res: Int)
ensures (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 1))) // P1
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
var time1 : Int
var time2 : Int
time1 := ora(o1);
time2 := ora(o2);
var tmp : Int
tmp := Int_compare(time1, time2)
if (tmp == 0){
tmp := Int_compare(volume_totale(o1), volume_totale(o2))
if (tmp > 0){
return(1)
} else {
return(-1)
}
} else {
return(tmp)
}
assert returned
}