State
state′
slide
:
The specification of a
Counter
in Z