Ninth Asia-Pacific Software Engineering Conference (APSEC'02)
Refining Object-Oriented Invariants and Dynamic Constraints
Gold Coast, Australia
December 04-December 06
ISBN: 0-7695-1850-8
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.
Index Terms:
Object-orientation, refinement calculus, invariants, history properties.
Citation:
Jamie Shield, Ian J. Hayes, "Refining Object-Oriented Invariants and Dynamic Constraints," apsec, pp.52, Ninth Asia-Pacific Software Engineering Conference (APSEC'02), 2002