Word_true
Word, correct 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
}
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(o2, 1) && rel(o2, 0) == rel(o1, 1)
ensures (sgn(rel(res, 0)) == -sgn(rel(res, 1))) // P1
{
var returned : Bool
returned := false
var left : Int
var right : Int
left := count(o1);
right := count(o2);
if (left == right){
var i : Int
i := 0;
while ((i < length(o1)) && (i < length(o2)) && !returned)
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(returned, 0) == rel(returned, 1))
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> (rel(i, 0) == rel(i, 1))
invariant (rel(o1, 0) == rel(o2, 1) && rel(o2, 0) == rel(o1, 1)) ==> ((rel(returned, 0) && rel(returned, 1)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 1))))
{
if((get(o1, i) - get(o2, i)) < 0){
return(-1)
}elseif((get(o1, i) - get(o2, i)) > 0){
return(1)
}else{
i := i + 1
}
}
if (!returned) {
return(length(o1) - length(o2));
}
}
else {
return((left > right)? 1:-1)
}
assert returned
}