TextPosition_false
TextPosition, incorrect 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 x1 : Rational
x1 := getXDirAdj(o1);
var x2 : Rational
x2 := getXDirAdj(o2);
var pos1YBottom : Rational
pos1YBottom := getYDirAdj(o1);
var pos2YBottom : Rational
pos2YBottom := getYDirAdj(o2);
// note that the coordinates have been adjusted so 0,0 is in upper left
var pos1YTop : Rational
pos1YTop := pos1YBottom - getHeightDir(o1);
var pos2YTop : Rational
pos2YTop := pos2YBottom - getHeightDir(o2);
var yDifference : Rational
yDifference := abs(pos1YBottom-pos2YBottom)
//we will do a simple tolerance comparison.
if( yDifference < 1/1 ||
(pos2YBottom >= pos1YTop && pos2YBottom <= pos1YBottom) ||
(pos1YBottom >= pos2YTop && pos1YBottom <= pos2YBottom))
{
if( x1 < x2 )
{
retval := -1;
}
else {
if( x1 > x2 )
{
retval := 1;
}
else
{
retval := 0;
}
}
}
elseif( pos1YBottom < pos2YBottom )
{
retval := -1;
}
else
{
return(1)
}
if (!returned) {
return(retval)
}
}
assert returned
}