package Counter
   --# own Count : Integer;
   --# initializes Count;
is
   procedure Reset(Value: in Integer);
   --# global out Count;
   --# derives Count from Value;

   procedure Inc;
   --# global in out Count;
   --# derives Count from Count;

   procedure Dec;
   --# global in out Count;
   --# derives Count from Count;

   function Value return Integer;
   --# global in Count;

end Counter;