class interface COUNTER
   --
   -- Simple counter object (useful as a once function).
   --

feature(s) from COUNTER   value: INTEGER
      -- The value of the counter.


   increment
      ensure
         value = 1 + old value

   decrement
      ensure
         value + 1 = old value

   reset
      ensure
         value = 0

   append_in (buffer: STRING)
      -- Append the value of the counter in the buffer.




end of COUNTER