# A tool for data refinement

## 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

Proof Obligation Data Refinement Weak Precondition Predicate Transformer Program Refinement## Preview

Unable to display preview. Download preview PDF.

## References

- 1.R. J. Back.
*Correctness Preserving Program Refinements: Proof Theory and Applications*, volume 131 of*Mathematical Center Tracts*. Mathematical Centre, Amsterdam, 1980.Google Scholar - 2.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.Google Scholar - 3.R. J. Back and K. Sere. Stepwise refinement of action systems.
*Structured Programming*, 12:17–30, Sept. 1991.Google Scholar - 4.R. J. Back and J. von Wright. Reasoning algebraically about loops. Technical Report 144, Turku Centre for Computer Science, November 1997.Google Scholar
- 5.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.Google Scholar - 6.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.Google Scholar - 7.E. W. Dijkstra.
*A Discipline of Programming*. Prentice-Hall Series in Automatic Computation. Prentice Hall, 1976.Google Scholar - 8.M. J. C. Gordon and T. F. Melham, editors.
*Introduction to HOL: A theorem proving environment for higher order logic*. Cambridge University Press, 1993.Google Scholar - 9.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.Google Scholar - 10.J. Grundy. The HOL window library. In
*The HOL System*, volume Libraries. SRI International, Cambridge, England, 2.01 edition, July 1991.Google Scholar - 11.C. A. R. Hoare. Proof of correctness of data representations.
*Acta Informatica*, 1(4):271–281, 1972.zbMATHCrossRefGoogle Scholar - 12.C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design.
*Acta Informatica*, 30(8):701–739, 1993.zbMATHMathSciNetCrossRefGoogle Scholar - 13.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.Google Scholar - 14.C. B. Jones.
*Systematic Software Development using VDM*. Prentice-Hall, 1986.Google Scholar - 15.L. Laibinis and J. von Wright. Context handling in the refinement calculus framework. Technical Report 118, Turku Centre for Computer Science, June 1997.Google Scholar
- 16.P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report TR 25.085, IBM Laboratory Vienna, 1968.Google Scholar
- 17.C. C. Morgan. Auxiliary variables in data refinement.
*Information Processing Letters*, 29:293–296, 1988.zbMATHMathSciNetCrossRefGoogle Scholar - 18.C. C. Morgan.
*Programming from Specifications*. Prentice Hall, 2nd edition, 1994.Google Scholar - 19.C. C. Morgan and P. H. Gardiner. Data refinement by calculation.
*Acta Informatica*, 27(6):481–503, 1990.zbMATHMathSciNetCrossRefGoogle Scholar - 20.J. M. Morris. Laws of data refinement.
*Acta Informatica*, 26(4):287–308, 1989.zbMATHMathSciNetGoogle Scholar - 21.J. K. Ousterhout.
*Tcl and the Tk Toolkit*. Addison Wesley, 1994.Google Scholar - 22.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.Google Scholar - 23.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.Google Scholar