SSL workspace.vdmpp  Sprache: unbekannt

class WorkSpace is subclass of Vector
 
  types
    Token = nat;

  instance variables
    screen: map Token to Quadrilateral := {|->};
 
  operations

    LookUp: Token ==> Quadrilateral
    LookUp(qid) ==
      return screen (qid)
    pre qid in set dom screen;

    GetAngle: Token ==> real
    GetAngle(qid) ==
      def scrn: Parallelogram = screen(qid) in
        return scrn.GetAngle()
    pre qid in set dom screen 
        and isofclass (Parallelogram, screen(qid));
 
    Display: Token * Quadrilateral ==> ()
    Display(qid, q) == 
      ( screen := screen munion { qid |-> q };
        q.Display() )
    pre q not in set rng screen;

    UnDisplay: Token ==> ()
    UnDisplay(qid) == 
      screen := {qid} <-: screen
    pre qid in set dom screen;

    Move: Token * (nat * nat) * (nat * nat) ==> ()
    Move(qid, p1, p2) ==
    ( dcl scrn : Quadrilateral := screen(qid);
      UnDisplay (qid);
      scrn.Move (p1,p2);
      Display (qid, scrn)
    )
    pre qid in set dom screen
  
end WorkSpace