Algorithm refinement with read and write frames

Abstract

The read and write frames of reference variables used in the VDM style of operation decomposition serve two purposes. Syntactically, they bind the variables that occur in the predicates of the operation specification; and semantically, they record what access to the state an implementation can be allowed to make. This paper examines the use of frames in these two roles, in particular considering the case when there is an invariant on the state. It argues that the two roles can be usefully distinguished.

A model for operation specification and refinement is developed where full account is taken of both syntactic and semantic roles of the frames. Consideration of their syntactic role gives rise to the idea that a part of the state can be independent of the rest with respect to the invariant that is in force: a definition of independence is given together with a syntactic sufficient-condition for it. The semantic role of the frames is examined in connection with notions of satisfiability and satisfaction. Satisfiability is modified to capture the restricted possible interdependencies between read and write variables and the rules for satisfaction are given that restrict the usual relation in order to respect the constraints on implementations imposed by the frames.