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