Contact_false
Contact, incorrect version
function getFirstName(self: Ref) : Int
function getLastName(self: Ref) : Int
function getEmails(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 String_compareIgnoreCase(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
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
var compareFirstName : Int := 0
if ((getFirstName(o1) != 0) && (getFirstName(o2) != 0)) {
compareFirstName := String_compareIgnoreCase(getFirstName(o1), getFirstName(o2));
if (compareFirstName == 0) {
var compareLastName : Int := 0
if ((getLastName(o1) != 0) && (getLastName(o2) != 0)) {
compareLastName := String_compareIgnoreCase(getLastName(o1), getLastName(o2));
if (compareLastName == 0) {
var compareEmail : Int := 0
if ((getEmails(o1) != 0) && (getEmails(o2) != 0)) {
compareEmail := String_compareIgnoreCase(getEmails(o1), getEmails(o2));
return(compareEmail)
} else {
return(0)
}
} else {
return(compareLastName)
}
} else {
var compareEmail : Int := 0
if ((getEmails(o1) != 0) && (getEmails(o2) != 0)) {
compareEmail := String_compareIgnoreCase(getEmails(o1), getEmails(o2));
return(compareEmail)
} else {
return( 0)
}
}
} else {
return(compareFirstName)
}
} else {
var compareLastName : Int := 0
if ((getLastName(o1) != 0) && (getLastName(o2) != 0)) {
compareLastName := String_compareIgnoreCase(getLastName(o1), getLastName(o2));
if (compareLastName == 0) {
var compareEmail : Int := 0
if ((getEmails(o1) != 0) && (getEmails(o2) != 0)) {
compareEmail := String_compareIgnoreCase(getEmails(o1), getEmails(o2));
return(compareEmail)
} else {
return(0)
}
} else {
return(compareLastName)
}
} else {
var compareEmail : Int := 0
if ((getEmails(o1) != 0) && (getEmails(o2) != 0)) {
compareEmail := String_compareIgnoreCase(getEmails(o1), getEmails(o2));
return(compareEmail)
} else {
return(0)
}
}
}
assert returned
}