// @(#)$Id: Button.h,v 1.5 1997/07/25 22:49:18 leavens Exp $

//@ uses ButtonTrait;
//@ spec class MouseLocation;
//@ spec class MouseClick;

class Button {
public:
  //@ spec MouseLocation loc;
  //@ spec MouseClick click;

  Button() throw();
  //@ behavior {
  //@   modifies loc, click;
  //@   ensures loc' = out /\ click' = up;
  //@ }

  virtual void MouseEnter() throw();
  //@ behavior {
  //@   modifies loc;
  //@   ensures loc' = in;
  //@ }

  virtual void MouseLeave() throw();
  //@ behavior {
  //@   modifies loc;
  //@   ensures loc' = out;
  //@ }

  virtual void MouseUp() throw();
  //@ behavior {
  //@   modifies click;
  //@   ensures click' = up;
  //@ }

  virtual void MouseDown() throw();
  //@ behavior {
  //@   modifies click;
  //@   ensures click' = down;
  //@ }

};

[Index]

HTML generated using lcpp2html.