class interface COUNTER
feature(s) from COUNTER
   value: INTEGER
   increment
      ensure
         value = 1 + old value
   decrement
      ensure
         value + 1 = old value
   reset
      ensure
         value = 0
   append_in (str: STRING)
end of COUNTER