Benjam

CONSTANTS
        x0,
        deltaX,
        y0,
        deltaY
PROPERTIES
    x0:NAT &
    x0<=MAXINT &
    x0>=0&
    deltaX:NAT &
    x0+deltaX<=MAXINT &
    y0:NAT &
    y0<=MAXINT &
    y0>=0 &
    deltaY:NAT &
    y0+deltaY<=MAXINT
VARIABLES
    xx,
    yy
INVARIANT
    xx:NAT & deltaX+x0>=xx
&   yy:NAT & deltaY+y0>=yy
INITIALISATION
    xx:=0
||    yy:=0

OPERATIONS
   setX(nx)=
       PRE nx:NAT & nx<= MAXINT & nx<=deltaX+x0
       THEN xx:=nx
   END;

   incX(val)=
       PRE val:NAT & val<=MAXINT & xx+val<=MAXINT & val+xx<=deltaX+x0
       THEN xx:= val+xx
   END;

   decrX(val)=
       PRE val:NAT & val<=MAXINT & xx-val>=x0
       THEN xx:= xx-val
   END;

   setY(ny)=
       PRE ny:NAT & ny<= MAXINT & ny<=deltaY+y0
       THEN yy:=ny
   END;

   incY(val)=
       PRE val:NAT & val<=MAXINT & yy+val<=MAXINT & val+yy<=deltaY+y0
       THEN yy:= val+yy
   END;

   decrY(val)=
       PRE val:NAT & val<=MAXINT & yy-val>=y0
       THEN yy:= yy-val
   END;

   val<--getX=
       BEGIN
           val:=xx
   END;

   val<--getY=
       BEGIN
           val:=yy
   END;

   val<--borneX(ux)=
       PRE ux:NAT
       THEN
           val:=bool(ux>=x0 & ux<=x0+deltaX)
   END;

   val<--borneY(uy)=
       PRE uy:NAT
       THEN
           val:=bool(uy>=x0 & uy<=x0+deltaY)
   END