TextPosition_true
TextPosition, correct version
function getDir(self: Ref) : Int
function getYDirAdj(self: Ref) : Int
function getXDirAdj(self: Ref): Int
function getHeightDir(self: Ref) : Int
function getWidthDirAdj(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
function abs(i: Int) : Int
{
i < 0 ? -i : i
}
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 retval : Int
retval := 0;
/* Only compare text that is in the same direction. */
if (getDir(o1) < getDir(o2))
{
return(-1)
}elseif (getDir(o1) > getDir(o2))
{
return(1)
}else{
// Get the text direction adjusted coordinates
var pos1YBottom: Int
var pos2YBottom : Int
pos1YBottom := getYDirAdj(o1);
pos2YBottom := getYDirAdj(o2);
// note that the coordinates have been adjusted so 0,0 is in upper left
var aux : Int
var yDifference : Int
aux := pos1YBottom-pos2YBottom;
yDifference := abs(aux)
//we will do a simple tolerance comparison.
if (yDifference < 1)
{
var x1 : Int
x1 := getXDirAdj(o1);
var x2 : Int
x2 := getXDirAdj(o2);
aux := x1-x2;
var xDifference : Int
xDifference := abs(aux)
if (xDifference < 1)
{
var pos1Height : Int
pos1Height := getHeightDir(o1);
var pos2Height : Int
pos2Height := getHeightDir(o2);
aux := pos1Height - pos2Height;
var heightDifference : Int
heightDifference := abs(aux)
if (heightDifference < 1)
{
var pos1Width : Int
pos1Width := getWidthDirAdj(o1);
var pos2Width : Int
pos2Width := getWidthDirAdj(o2);
aux := pos1Width - pos2Width;
var widthDifference : Int
widthDifference := abs(aux)
if (widthDifference < 1)
{
retval := 0;
}
else
{
retval := pos1Width < pos2Width ? -1 : 1;
}
}
else
{
retval := pos1Height < pos2Height ? -1 : 1;
}
}
else
{
retval := x1 < x2 ? -1 : 1;
}
}
else
{
retval := pos1YBottom < pos2YBottom ? -1 : 1;
}
return(retval)
}
assert returned
}