CatBPos_false
CatBPos, incorrect version
function getHdopBPosGetTime(self: Ref) : Int
function getBPosGetTime(self: Ref) : Int
function getBPosGetStat(self: Ref) : Int
//function getBPosIsDeparture(self: Ref) : Bool
function getBPosIsVacation(self: Ref) : Bool
function getBPosIsDeparture(self: Ref) : Bool
function getBPosIsArrival(self: Ref) : Bool
function getHdopBPosGetTimeIsNotVoid(self: Ref) : Bool
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
ensures (rel(o1, 0) == rel(o2, 2) && rel(o2, 0) == rel(o1, 2)) ==> (sgn(rel(res, 0)) == -sgn(rel(res, 2))) // P1
ensures (rel(o1, 2) == rel(o2, 1) && rel(o2, 2) == rel(o1, 1)) ==> (sgn(rel(res, 2)) == -sgn(rel(res, 1))) // P1
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(res, 0) > 0) && rel(res, 1) > 0 && rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1)) ==> (rel(res, 2) > 0) // P2
ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 0) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 2)))
ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 1) == 0) ==> (sgn(rel(res, 0)) == sgn(rel(res, 2)))
ensures (rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) && rel(res, 2) == 0) ==> (sgn(rel(res, 1)) == sgn(rel(res, 0)))
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 lCompare : Int
var returned : Bool
returned := false
if (getHdopBPosGetTimeIsNotVoid(o1) && getHdopBPosGetTimeIsNotVoid(o2)) {
lCompare := Int_compare(getHdopBPosGetTime(o1), getHdopBPosGetTime(o2));
if (lCompare != 0) {
res := lCompare
returned := true
}
}
if (!returned) {
lCompare := Int_compare(getBPosGetTime(o1), getBPosGetTime(o2));
if (lCompare != 0) {
res := lCompare;
returned := true
}
if (!returned) {
if (getBPosIsDeparture(o1) && getBPosIsVacation(o2)) {
res := 1
returned := true
} else {
if (getBPosIsVacation(o1) && getBPosIsArrival(o2)) {
res := 1
returned := true
}
}
// Ankunft und Abfahrt für denselben Bahnhof sollen in der richtigen Reihenfolge sein
if (!returned && getBPosIsDeparture(o1) && getBPosIsArrival(o2) && (getBPosGetStat(o1) == getBPosGetStat(o2))) {
res := 1
returned := true
}else{
res := 0
returned := true
}
}
}
assert returned
}