Behavioral properties

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

Types as Behavior