NameComparator_true
NameComparator, correct version
function Name(self: Ref) : Int
function strNames(): Seq[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(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(o1, 0) == rel(o1, 1) && rel(o2, 0) == rel(o1, 2) && rel(o2, 2) == rel(o2, 1) && rel(res, 0) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 2)))
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 x : Int
x := Name(o1)
var y: Int
y := Name(o2)
if(x == y){
return(0)
}else{
var i : Int
i := 0
var currentName : Int
while(i < |strNames()| && !returned)
invariant i >= 0 && i <= |strNames()|
invariant returned ==> res != 0
invariant (forall j : Int :: j >= 0 && j < i ==> (strNames()[j] != x && strNames()[j] != y))
invariant returned && res > 0 ==> i < |strNames()| && strNames()[i] == x
invariant returned && res < 0 ==> i < |strNames()| && strNames()[i] == y
{
currentName := strNames()[i]
if(currentName == x) {
return(1)
}else{
if(currentName == y) {
return(-1)
}else{
i := i + 1
}
}
}
assume returned
if (!returned) {
var tmp : Int
tmp := Int_compare(x,y)
return(tmp)
}
}
assert returned
}