Container_true
ArrayInt, correct 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 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 rv : Int
// Times
rv := Int_compare(departureTime(o1), departureTime(o2));
assert ((rel(rv, 0) > 0) && rel(rv, 1) > 0 && rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)) ==> (rel(rv, 2) > 0)
if (rv == 0) {
// Duration
if (departureMaxDuration(o1) < departureMaxDuration(o2)) {
rv := -1;
}
else{
if (departureMaxDuration(o1) > departureMaxDuration(o2)) {
rv := 1;
}
/*else {
// Transport company
rv := Int_compare(departureTransportCompany(o1), departureTransportCompany(o2));
assert ((rel(rv, 0) > 0) && rel(rv, 1) > 0 && rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)) ==> (rel(rv, 2) > 0)
if (rv == 0) {
// Transport type
rv := Int_compare(departureTransportType(o1), departureTransportType(o2));
assert ((rel(rv, 0) > 0) && rel(rv, 1) > 0 && rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)) ==> (rel(rv, 2) > 0)
}
}*/
}
}
return(rv)
assert returned
}