FileItem_false

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 String_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 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 var restmp : Int := 0 if ((o1 != null) && (o2 != null)) { var n1 : Ref n1 := getFileName(o1) var n2 : Ref n2 := getFileName(o2); if ((n1 != null) && (n2 != null)) { restmp := String_compare(n1, n2); } } return(restmp) assert returned }