NzbFile_true
NzbFile, correct version
function getFileName(self: Ref) : Ref
function getFileName_toLowerCase_endsWith(self: Ref, str: Int) : Bool
function getSubject(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
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(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 String_compare(o1: Ref, o2: Ref) 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(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
if (o1 == o2) {
return(0)
}else{
if ((getFileName(o1) != null) && (getFileName(o2) != null)){
var i : Int
i := 0;
while (i < 5 && !returned)
invariant i >= 0 && i <= 5
invariant (forall j : Int :: j >= 0 && j < i ==> (!getFileName_toLowerCase_endsWith(o1, j) && !getFileName_toLowerCase_endsWith(o2, j)))
invariant returned && res > 0 ==> i < 5 && getFileName_toLowerCase_endsWith(o2, i) && !getFileName_toLowerCase_endsWith(o1, i)
invariant returned && res < 0 ==> i < 5 && !getFileName_toLowerCase_endsWith(o2, i) && getFileName_toLowerCase_endsWith(o1, i)
invariant returned && res == 0 ==> i < 5 && getFileName_toLowerCase_endsWith(o2, i) && getFileName_toLowerCase_endsWith(o1, i)
{
if(getFileName_toLowerCase_endsWith(o1, i) && getFileName_toLowerCase_endsWith(o2, i)){
return(0)
}
elseif(getFileName_toLowerCase_endsWith(o1, i)){
return(-1000 + i)
}
elseif(getFileName_toLowerCase_endsWith(o2, i)){
return(1000 + i)
}else{
i := i + 1
}
}
if (!returned){
var tmp: Int
tmp := String_compare(getFileName(o1), getFileName(o2))
return(tmp)
}
}
elseif ((getFileName(o1) != null) && (getFileName(o2) == null))
{
return(-995)
}
elseif ((getFileName(o1) == null) && (getFileName(o2) != null))
{
return(1005)
}
else
{
var tmp: Int
tmp := Int_compare(getSubject(o1), getSubject(o2))
return(tmp)
}
}
assert returned
}