DataPoint_false
DataPoint, incorrect version
function fiscalQuarter(self: Ref) : Int
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 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
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 fiscalResult : Int
fiscalResult := Int_compare(fiscalQuarter(o1),fiscalQuarter(o2));
if (fiscalResult > 0) {
return(fiscalResult)
}else{
if (fiscalResult < 0) {
return(fiscalResult)
} else {
if (sectorCode(o1) > 0) {
if (sectorCode(o1) > sectorCode(o2)) {
return(sectorCode(o1) - sectorCode(o2))
}
else {
if (sectorCode(o1) < sectorCode(o2)){
return(sectorCode(o2) - sectorCode(o1))
} else {
return(0) // Should never happen
}
}
} else {
if (industryCode(o1) > 0) {
if (industryCode(o1) > industryCode(o2)) {
return(industryCode(o1) - industryCode(o2))
}
else {
if (industryCode(o1) < industryCode(o2)) {
return(industryCode(o2) - industryCode(o1))
} else {
return(0) // Should never happen
}
}
}// These should never be reached
else {
if (sectorCode(o1) > 0) {
return(-1)
} else {
if (industryCode(o2) > 0) {
return( -1)
} else {
return(0)
}
}
}
}
}
}
assert returned
}