SSL Position.vdmrt   Sprache: VDM

\section{Position Class}

\begin{vdm_al}
-----------------------------------------------
-- Class: Position
-- Description:  Defines a X,Y position
-----------------------------------------------

--
-- class definition
--
class Position

--
-- instance variables
--
instance variables

private x: int;
private y: int;

--
-- Types definition section
--
types   

--
-- Operations definition section
--
operations

public Position: int * int ==> Position
Position(x_, y_) ==
(
 x := x_;
 y := y_;
);
  
pure public X: () ==> int
X() ==
(
 return x;
);

pure public Y: () ==> int
Y() ==
(
 return y;
);

public setX : int ==> ()
setX(newX) ==
(
  x := newX

);

public setY: int ==> ()
setY(newY) ==
(
y := newY

);

public toString : () ==> seq of char
toString() == 
(
 return "position X: " 
 ^ Printer`intToString(x) 
 ^ " Y: " ^ Printer`intToString(y) 
);

pure public inRange : Position * int ==> bool
inRange(p, range) ==
(
return (abs(x -p.X()) <= range) and (abs(y -p.Y()) <= range);  
);

pure public deepCopy : () ==> Position
deepCopy() ==
(
 let newPos = new Position(x,y)
 in 
 return newPos;  
)

--
-- Functions definition section
--
functions
public static Compare: Position * Position -> bool
Compare(a,b) ==
a.X() = b.X() and a.Y() = b.Y() 


--
-- Values definition section
--
values

end Position

\end{vdm_al}

\begin{rtinfo}
[TotalxCoverage]{vdm.tc}[Position]
\end{rtinfo}