Abstract
Data refinement is a powerful technique to derive implementations in terms of low-level data structures like bytes from specification in terms of high-level data structures like queues. The higher level operations need not be coded as ordinary programs; it is more convenient to introduce specification statements to the programming language and use them instead of actual code. Specification statements represent the maximal program satisfying a given Hoare-triple. Sound and (relatively) complete simulation techniques allow for proving data refinement by local arguments. A major challenge for simulation consists of expressing the weakest lower level specification simulating a given higher level specification w.r.t. a given relation between these two levels of abstraction. We present solutions to this challenge for upward and downward simulation in both partial and total correctness frameworks, thus reducing the task of proving data refinement to proving validity of certain Hoare-triples.
Supported by ESPRIT BRA project REACT (no.6021).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. J. Back and J. von Wright. Refinement calculus, part I: Sequential nondeterministic programs. In Stepwise Refinement of Distributed Systems, volume 430 of LNCS, pages 43–66,1990.Springer-Verlag.
J. Coenen, J. Zwiers, and W.-P. de Roever. Assertional data reification proofs: Survey and perspective. In J. Morris and R. Shaw, editors, Proceedings of the 4th Refinement Workshop, Workshops in Computing, pages 91–114. Springer-Verlag, 1991.
P. Cousot. Handbook of Theoretical Computer Science: Formal Models and Semantics, volume B, chapter 15, pages 841–993. Elsevier/MIT Press, 1990.
E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453–457, 1975.
K. Engelhardt, W.-P. de Roever, et al. Data refinement. submitted to Prentice-Hall, an annotated table of contents is available at http://www.informatik.uni-kiel.de/∼ke/proposal.ps.
P. Gardiner. Algebraic proofs of consistency and completeness. FACS, 1994. submitted.
P. H. Gardiner and C. Morgan. Data refinement of predicate tranformers. Theoretical Computer Science, (87):143–162, 1991.
P. H. Gardiner and C. Morgan. A single complete rule for data refinement. Formal Aspects of Computing, 5:367–382, 1993.
C. Hoare. Proofs of correctness of data representation. Acta Informatica, 1:271–281, 1972.
C. Hoare, He J., and J. Sanders. Prespecification in data refinement. Information Processing Letters, 25:71–76, 1987.
C. Morgan and T. Vickers. On the Refinement Calculus. Springer-Verlag, 1994.
J. M. Morris. Laws of data refinement. Acta Informatica, 26:287–308, 1989.
E.-R. Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 24:337–347, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Engelhardt, K., de Roever, WP. (1996). Simulation of specification statements in Hoare logic. In: Penczek, W., Szałas, A. (eds) Mathematical Foundations of Computer Science 1996. MFCS 1996. Lecture Notes in Computer Science, vol 1113. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61550-4_159
Download citation
DOI: https://doi.org/10.1007/3-540-61550-4_159
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61550-7
Online ISBN: 978-3-540-70597-0
eBook Packages: Springer Book Archive