<s5>Æliens</s5> -- slide(s)

Subtype requirements -- signature and behavior

preservation of behavioral properties

Safety properties -- nothing bad

invariant properties -- true of all states
history properties -- true of all execution sequences

slide: Subtyping and behavior

Example -- $IntSet \not<= FatSet$

FatSet -- insert, select, size
IntSet -- insert, delete, select, size

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}$

slide: History properties -- example

Types as behavior -- constraints

$x : 9..11$ $<=>$ $x : Int /\ 9 <= x <= 11$

Behavioral constraints -- signature versus assertions

$f(x:9..11) : 3..5 { ... }$


    int f(int x) {
       require( 9 <= x  && x <= 11 );
       ...
       promise( 3 <= result && result <= 5);
       return result;
       }

slide: Types and behavioral constraints