Match_true
Match, correct version
function score(self: Ref) : Int
function seq1start(self: Ref) : Int
function seq2start(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(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
// first compare scores
if (score(o1) > score(o2)) {
return(-1) /* higher score for o1 -> o1 */
}else{
if (score(o1) < score(o2)){
return(1) /* higher score for o2 -> o2 */
}else{
// scores are equal, go on with the position
if ((seq1start(o1) + seq2start(o1)) < (seq1start(o2) + seq2start(o2))) {
return(-1) /* o1 is farther left */
}else{
if ((seq1start(o1) + seq2start(o1)) > (seq1start(o2) + seq2start(o2))) {
return(1) /* o2 is farther left */
}else{
// they're equally good
return(0)
}
}
}
}
assert returned
}