language: en

[127]

Progress for Local Variables in UNITY

Rob Udink and Ted Herman and Joost Kok
Department of Computer Science, Utrecht University,
P.O. Box 80089, 3508 TB Utrecht, The Netherlands
e-mail: frob,ted,joostg@cs.ruu.nl

A new notion of refinement for UNITY programs with local variables is defined. This notion is compositional in the following sense: programs can be refined in arbitrary contexts such that all unless and leadsto properties (i.e. temporal properties for both safety and progress) of the composition are preserved. The refinement notion is based on preservation of a new kind of UNITY-like property that takes into account the locality of variables. We do a small case study about registers.

[Keyword Codes: F.3.1]

Keywords: Specifying and Verifying and Reasoning about Programs

1. INTRODUCTION