type Shape
{
   model:
      boolean covers(Point p);
   interface:
      void move(Vector to);
      void resize(int percent);
   action specs:
      move(Vector to)
      {
         true :- for_all p . old(covers(p)) <=> covers(p+to))
      }
      resize(int percent)
      {
         percent>0 :- for_all p . there_is centre . 
         old(covers(p-centre))) <=> covers((p-centre)*percent/100)
      }
   invariants:
};