Title: A theory of refinement for ADT's with functional interfaces



Authors: Sumesh Divakaran, Deepak D'Souza, Prahladavaradan Sampath, Nigamanth Sridhar, and Jim Woodcock.

Abstract: We propose a theory of refinement for Abstract Data Types (ADTs) that interact with client programs via function calls. Our notion of refinement is in the spirit of Z/VDM. We provide a simulation-based refinement condition similar to that of He et al.'s ``upward simulation'', and argue that it is both sound and complete for deterministic ADTs. Our theory also facilitates compositional reasoning about complex implementations that may use several layers of sub-ADTs.

pdf