Word_false
Word, incorrect version
function count(self: Ref) : Int
function length(self: Ref) : Int
function get(self: Ref, i: Int): Int
define return(x) {
assert !returned
returned := true
res := x
}
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
ensures (rel(o1, 0) == rel(o2, 2) && rel(o2, 0) == rel(o1, 2)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 2))) // P1
ensures (rel(o1, 2) == rel(o2, 1) && rel(o2, 2) == rel(o1, 1)) ==> (sgn(rel(res, 2)) == -sgn(rel(res, 1))) // P1
ensures (rel(o1, 0) == rel(o1, 1) && rel(o2, 0) == rel(o2, 1)) ==> (rel(res, 0) == rel(res, 1)) // deterministic
ensures (rel(o1, 0) == rel(o1, 2) && rel(o2, 0) == rel(o2, 2)) ==> (rel(res, 0) == rel(res, 2)) // deterministic
ensures (rel(o1, 2) == rel(o1, 1) && rel(o2, 2) == rel(o2, 1)) ==> (rel(res, 2) == rel(res, 1)) // deterministic
ensures ((rel(res, 0) > 0) && rel(res, 1) > 0 && rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)) ==> (rel(res, 2) > 0) // P2
ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 0) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 2)))
ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 1) == 0) ==> (sgn(rel(res, 0)) == sgn(rel(res, 2)))
ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 2) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 0)))
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
var tmp : Int
var left : Int
var right : Int
left := count(o1);
right := count(o2);
if (left == right) {
if(length(o1) > length(o2)){
var i1 : Int
i1 := 0;
while (i1 < length(o1) && !returned){
tmp := Int_compare(get(o1, i1), get(o2, i1))
if(tmp < 0){
return(1)
}else{
i1 := i1 + 1
}
}
if (!returned){
return(-1)
}
}
else {
var i2 : Int
i2 := 0;
while(i2 < length(o2) && !returned)
{
tmp := Int_compare(get(o1, i2), get(o2, i2))
if(tmp < 0){
return(-1)
}else{
i2 := i2 + 1;
}
}
if (!returned){
return(1)
}
}
}
else{
return((left > right)? 1:-1);
}
assert returned
}