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