Supporting module reuse in refinement

For the rigorous development of larger-scale software, the use of data abstractions is essential. For formal development in methods such as the VDM, B and the refinement calculus such abstractions are encapsulated in a module with state and operations. The principle of information hiding suggests that the state of a module should be inaccessible to the rest of a program. As an approach to refinement where an existing module is to be reused, we recommend relaxing the principle of information hiding to allow the program being developed to access the abstract state of the module directly. Eventually all references to the module state must be replaced by calls to module operations, but in the initial stages of refinement allowing only module operations is too restrictive. By allowing access to the module state the development method supports the reuse of existing modules more easily.