FileItem_true
FileItem, correct version
function getFileName(self: Ref) : Ref
function sectorCode(self: Ref) : Int
function industryCode(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 FileItem_compare(o1: Ref, o2: Ref) 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
if (o1 == null) {
if (o2 == null) {
return(0)
} else {
return(1) // this will put null in the end
}
} else{
if (o2 == null) {
return(-1)
}else {
var n1 : Ref
n1 := getFileName(o1);
var n2 : Ref
n2 := getFileName(o2);
if (n1 == null) {
if (n2 == null) {
return(0)
} else {
return(1) // this will put null names after non null names
}
} else {
if (n2 == null) {
return(-1)
}else{
var tmp : Int
tmp := FileItem_compare(n1, n2)
return(tmp)
}
}
}
}
assert returned
}