#### Signature

$%s <= %t$

• $dom\left( m_\left\{%t\right\} \right) <= dom\left( m_\left\{%s\right\} \right)$
• $ran\left( m_\left\{%s\right\} \right) <= ran\left( m_\left\{%t\right\} \right)$

#### Behavior

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

#### Extension -- diamond rule

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

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

slide: Behavioral subtyping constraints