5

• global invariants -- dynamic aliasing
• model-based specification -- state and operations
• compositions -- contracts, scripts, interaction, joint actions