We review retrenchment as a liberalization of refinement, for the description of applications too rich (e.g. using continuous and infinite types) for refinement. A specialization of the notion, evolving retrenchment, is introduced, motivated by the need for an approximate, evolving notion of simulation. The focus of the paper is the case study, a substantial second-order linear control system. The design step from continuous to zero-order hold discrete system is expressible as an evolving retrenchment. Thus we demonstrate that the retrenchment approach can formalize the development of useful applications, which are outside the scope of refinement.
展开▼
