Abstract
Refinement is a transformational approach to program development. Replacing data structures and adding computations over a new data structure are important steps in many formal methods of program construction. We consider the calculational approach to such transformations within the refinement calculus framework. In the calculational approach, there is no need for inventing a new program; instead, it is constructed from the old one using an abstraction relation that is to hold between the old and new data structures. We describe the foundations of a tool supporting this approach which uses the HOL theorem-proving system as an inference engine. In the tool, a refinement theorem is automatically derived as a consequence of the program calculation. We illustrate our approach with two small case studies.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Preview
Unable to display preview. Download preview PDF.
References
R. J. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.
R. J. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.
R. J. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17–30, Sept. 1991.
R. J. Back and J. von Wright. Reasoning algebraically about loops. Technical Report 144, Turku Centre for Computer Science, November 1997.
M. J. Butler, J. Grundy, T. Långbacka, R. Rukšėnas, and J. von Wright. The Refinement Calculator: Proof support for program refinement. In L. Groves and S. Reeves, editors, Formal Methods Pacific'97, Discrete Mathematics and Theoretical Computer Science, 1997. Springer-Verlag.
D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. A tool for developing correct programs by refinement. In H. Jifeng, editor, BGS FACS 7th Refinement Workshop. Springer-Verlag, July 1996.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice Hall, 1976.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
L. J. Groves, R. G. Nickson, and M. Utting. A tactic driven refinement tool. In C. B. Jones, B. T. Denvir, and R. C. F. Shaw, editors, 5th Refinement Workshop, Workshops in Computing, pages 272–297, London, Jan. 1992. BCS-FACS, Springer-Verlag.
J. Grundy. The HOL window library. In The HOL System, volume Libraries. SRI International, Cambridge, England, 2.01 edition, July 1991.
C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271–281, 1972.
C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta Informatica, 30(8):701–739, 1993.
H.-M. JÄrvinen and R. Kurki-Suonio. DisCo specification language: marriage of actions and objects. in Proc. of 11th Int. Conf. on Distributed Computing Systems, pages 142–151, IEEE Computer Society, 1991.
C. B. Jones. Systematic Software Development using VDM. Prentice-Hall, 1986.
L. Laibinis and J. von Wright. Context handling in the refinement calculus framework. Technical Report 118, Turku Centre for Computer Science, June 1997.
P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report TR 25.085, IBM Laboratory Vienna, 1968.
C. C. Morgan. Auxiliary variables in data refinement. Information Processing Letters, 29:293–296, 1988.
C. C. Morgan. Programming from Specifications. Prentice Hall, 2nd edition, 1994.
C. C. Morgan and P. H. Gardiner. Data refinement by calculation. Acta Informatica, 27(6):481–503, 1990.
J. M. Morris. Laws of data refinement. Acta Informatica, 26(4):287–308, 1989.
J. K. Ousterhout. Tcl and the Tk Toolkit. Addison Wesley, 1994.
J. Shield, R. Nickson and D. Carrington. Supporting Data Refinement in a Program Refinement Tool. In L. Groves and S. Reeves, editors, Formal Methods Pacific'97, Discrete Mathematics and Theoretical Computer Science, 1997. Springer-Verlag.
J. von Wright. Program refinement by theorem prover. In D. Till and R.C.F. Shaw, editors, 6th Refinement Workshop, Workshops in Computing, pages 121–150, London, Jan. 1994. BCS-FACS, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rukšėnas, R., von Wright, J. (1998). A tool for data refinement. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055150
Download citation
DOI: https://doi.org/10.1007/BFb0055150
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive