topical media & game development
Types as behavior
1
subtype requirements
-- preservation of behavioral properties
behavioral properties
-- invariance, history
duality
-- static versus dynamic constraints
slide
:
Section 10.1: Types as behavior
Verifying behavioral properties
2
states
-- transformations
verification
-- correctness formulae
axioms
-- consequence rules, abstraction
slide
:
Section 10.2: Verifying behavioral properties
On the notion of behavior
3
syntax
-- expressions, statements
rules
-- assignment, object creation, method call
compound rules
-- composition, conditional, iteration
slide
:
Section 10.3: On the notion of behavior
Objects as behavioral types
4
abstract data types
-- representation function
correspondence
-- abstraction, renaming, extension
behavioral subtypes
-- correspondence
slide
:
Section 10.4: Objects as behavioral types
Specifying behavioral compositions
5
global invariants
-- dynamic aliasing
model-based specification
-- state and operations
compositions
-- contracts, scripts, interaction, joint actions
slide
:
Section 10.5: Specifying behavioral compositions