// @(#)$Id: QuadShape.h,v 1.17 1999/01/25 23:02:55 leavens Exp $
#ifndef QuadShape_h
#define QuadShape_h

#include "Vector.h"

//@ uses FourSidedFigure;

/*@ abstract @*/ class QuadShape {
public:
  //@ spec Vector edges[4];
  //@ spec Vector position;
  //@ invariant isLoop(edges\any);

  virtual Move(const Vector& v) throw();
  //@ behavior {
  //@   requires assigned(v, pre);
  //@   requires redundantly assigned(edges, pre)
  //@              /\ assigned(position, pre) /\ isLoop(edges^);
  //@   modifies position;
  //@   trashes nothing;
  //@   ensures liberally position' = position^ + v^;
  //@   ensures redundantly liberally edges' = edges^;
  //@   example liberally position^ = 0:Vector /\ position' = v^;
  //@ }

  virtual Vector GetVec(int i) const throw();
  //@ behavior {
  //@   requires between(1, i, 4);
  //@   ensures result = edges^[i-1];
  //@   example i = 1 /\ result = edges^[0];
  //@ }

  virtual Vector GetPosition() const throw();
  //@ behavior {
  //@   ensures result = position^;
  //@ }
};
#endif

[Index]

HTML generated using lcpp2html.