Container_false_v2
ArrayInt, incorrect, second version
function departureTimeIsBefore(self: Ref, t: Int) : Bool
function departureTime(self: Ref) : Int
function departureMaxDuration(self: Ref) : Int
function departureTransportCompany(self: Ref) : Int
function departureTransportType(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 compare(o1: Ref, o2: Ref) returns (res: Int)
requires rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)
ensures ((rel(res, 0) > 0) && rel(res, 1) > 0) ==> (rel(res, 2) > 0) // P2
{
var returned : Bool
returned := false
if (departureTimeIsBefore(o1, departureTime(o2))) {
return(-1)
}else{
if (departureTimeIsBefore(o1, departureTime(o2))) {
return(1)
}else{
if ((departureMaxDuration(o1) == departureMaxDuration(o2)) &&
(departureTransportType(o1) == departureTransportType(o2)) &&
(departureTransportCompany(o1) == departureTransportCompany(o2))) {
return(0)
}else {
return(1)
}
}
}
assert returned
}