Proof obligations
-- push/put
size( %a(s). elems ) < %a(s).bound
=>
length( s.items ) < s.limit
s' = << s.items \. i, s.limit >>
=>
%a(s')
=
<< %a(s).elems \uplus { i }, %a(s).bound >>
slide
:
Behavioral subtypes -- proof obligations