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.