Retrenchment and refinement interworking:the tower theorems

摘要

Retrenchment is a flexible model evolution formalism that compensates for the limitationsrnimposed by specific formulations of refinement. Its refinement-like proof obligations featurernadditional predicates for accommodating design data describing the model change. The bestrnresults are obtained when refinement and retrenchment cooperate, the paradigmatic schemernfor this being the commuting square or tower, in which ‘horizontal retrenchment rungs’rncommute with ‘vertical refinement columns’ to navigate through a much more extensiverndesign space than permitted by refinement alone. In practice, the navigation is accomplishedrnthrough ‘square completion’ constructions, and we present and prove a full suite of squarerncompletion theorems.