History property
-- not satisfied by $IntSet$
\A s : FatSet. \A %f, %q : State. %f < %q /\ s \e dom (%q).
\hspace{2cm}
\A x : Int. x \e s_{%f} => x \e s_{%q}
Objects as Behavioral Types
slide
:
History properties -- example
