State

Counter 


  
  \begin{schema}{Counter}
  n : \nat
  \where
  n \geq 0
  \end{schema}

Operations

 
  
  \begin{schema}{Incr}
  \Delta Counter
  \where
  \mbox{ $ n' = n + 1 $ }
  \end{schema}
  
  \begin{schema}{Decr}
  \Delta Counter
  \where
  n > 0 \\
  \mbox{ $ n' = n - 1 $ }
  \end{schema}
slide: The specification of a Counter in Z