topical slide(s): creative technology / new media / game development(s)

Signature

$%s <= %t$

$dom( m_{%t} ) <= dom( m_{%s} )$
$ran( m_{%s} ) <= ran( m_{%t} )$

Behavior

$pre( m_{%t} )[ x_{%t} := %a( x_{%s} )] => pre( m_{ %s } )$
$post( m_{ %s } ) => post( m_{ %t } )[ x_{ %t } := %a( x_{ %s } ) ]$
$invariant( %s )$ $=>$ $invariant( %t )[ x_{ %t } := %a( x_{ %s } ) ]$

Extension -- diamond rule

$%x(x.m(a)) = %p_{m}$

$%f \apijl{ x.m(a) } %f' /\ %f \apijl{ %p_{m} } %Q$
$=>$ $%a( x_{ %f } ) = %a( x_{ %Q } )$

slide: Behavioral subtyping constraints