Refining object-oriented invariants and dynamic constraints

An invariant is a constraint on a class which holds for each externally accessible state of its instances. A dynamic constraint is a dual-state property dictating before to after state behaviour that all methods must adhere to. Both invariants and dynamic constraints are of practical benefit as they allow explicit declaration of high-level behavioural constraints on a class and all its sub-classes. In this paper, formalisations of invariants and dynamic constraints are provided in the refinement calculus. Each is separated into coerced (specification) and extant (implemented or documentation) categories. Refinement rules are provided for strengthening invariants and dynamic constraints. Two separate development paths are identified: (behavioural) sub-classing and private refinement. Refining a class may violate its invariant or dynamic constraint. Sub-classing is a constrained form of refinement that maintains these properties. Revised refinement laws are provided. Private refinement is an alternative to (behavioural) sub-classing. It also maintains properties such as invariants and dynamics constraints and foregoes the constraints of sub-classing. The disadvantage is that private refinement can only be used to implement a class.