post( push(i) ) ⇒ post( put(i) )[ b : = α(s) ]
slide
:
Types and behavioral constraints