Behavioral refinement

Ultimately, types are meant to specify behavior in an abstract way. To capture behavioral properties, we will generalize our notion of types as constraints to include behavioral descriptions in the form of logical assertions.

Behavioral refinement

types as behavior
verification
abstraction and representation
behavioral compositions

Additional keywords and phrases: behavioral subtypes, state transformers, correctness formulae, assertion logic, transition systems, invariants, formal specification

slide: Behavioral refinement

In this chapter we will explore the notion of behavioral (sub)types. First we characterize the trade-offs between statically imposed (typing) constraints and dynamic constraints resulting from the specification of behavioral properties. We will provide a brief introduction to the assertion logic underlying the verification of behavioral constraints. Also, we look at how we may characterize the behavior of object-based systems in a mathematical way. Then we will describe the duality between abstraction and representation in defining behavioral subtypes that define concrete realizations of abstract specifications. In particular, we specify the correspondence requirements for behavioral subtypes. We will conclude this chapter by discussing the problems involved in specifying behavioral compositions, and explore what specification techniques are available to model the behavior of object-based systems.