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