A tool for data refinement

  • Rimvydas Rukšėnas
  • Joakim von Wright
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)


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.


Proof Obligation Data Refinement Weak Precondition Predicate Transformer Program Refinement 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 3.
    R. J. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17–30, Sept. 1991.Google Scholar
  4. 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. 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. 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. 7.
    E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice Hall, 1976.Google Scholar
  8. 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. 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. 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. 11.
    C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271–281, 1972.zbMATHCrossRefGoogle Scholar
  12. 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. 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. 14.
    C. B. Jones. Systematic Software Development using VDM. Prentice-Hall, 1986.Google Scholar
  15. 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. 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. 17.
    C. C. Morgan. Auxiliary variables in data refinement. Information Processing Letters, 29:293–296, 1988.zbMATHMathSciNetCrossRefGoogle Scholar
  18. 18.
    C. C. Morgan. Programming from Specifications. Prentice Hall, 2nd edition, 1994.Google Scholar
  19. 19.
    C. C. Morgan and P. H. Gardiner. Data refinement by calculation. Acta Informatica, 27(6):481–503, 1990.zbMATHMathSciNetCrossRefGoogle Scholar
  20. 20.
    J. M. Morris. Laws of data refinement. Acta Informatica, 26(4):287–308, 1989.zbMATHMathSciNetGoogle Scholar
  21. 21.
    J. K. Ousterhout. Tcl and the Tk Toolkit. Addison Wesley, 1994.Google Scholar
  22. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Rimvydas Rukšėnas
    • 1
    • 2
  • Joakim von Wright
    • 2
  1. 1.Turku Centre for Computer Science (TUCS)TurkuFinland
  2. 2.Dept. of Computer Scienceåbo Akademi UniversityTurkuFinland

Personalised recommendations