A framework for the stepwise refinement of UNITY programs with local variables is proposed. It is centered around two preorders. The first one compares program components with respect to a given context. Aside from being context-sensitive, this order also allows the introduction of local variables. The second preorder compares program contexts with respect to their discriminating power. Using these two relations, program refinement arises as a form of assumption/commitment reasoning. An example illustrates the use of the framework and presents some proof rules. The simple syntactic and semantic structure of UNITY allows for a natural game-theoretic characterization of the preorders used in the framework.
CITATION STYLE
Dinge, J. (1997). Approximating unity. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1282, pp. 320–337). Springer Verlag. https://doi.org/10.1007/3-540-63383-9_89
Mendeley helps you to discover research relevant for your work.