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