Lectures on Data Refinement

  • David Gries
Conference paper
Part of the NATO ASI Series book series (volume 88)


These lectures discuss the notion of data refinement: the replacement of one or more variables in a program by other variables, with suitable replacement of expressions and statements, to yield an equivalent program.


Coordinate Transformation Hash Table Predicate Calculus Conditional Statement Proof Obligation 
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]
    Aho, A.V., J.E. Hopcroft and J.D. Ullman. Date Structures and Algorithms. Addison-Wesley, Reading, 1985, 96–102.Google Scholar
  2. [2]
    Back, R.-J. On the correctness of refinement steps in program development. Report A-1978-4, Computer Science Department, University of Helsinki, 1978.Google Scholar
  3. [3]
    Chen, W., and J.T. Udding. Towards a calculus of data refinement. LNCS 375, Mathematics of Program Construction, Springer Verlag, New York, 1989.Google Scholar
  4. [4]
    Dijkstra, E.W. A Discipline of Programming. Prentice Hall, Englewood Cliffs, New Jersey, 1976.MATHGoogle Scholar
  5. [5]
    Dijkstra, E.W., and C.S. Scholten. Predicate Calculus and Program Semantics. Springer Verlag, New York, 1989.Google Scholar
  6. [6]
    Feijen, W.H.J., A.J.M. van Gasteren, and D. Gries. In-situ inversion of a cyclic permutation. IPL 24, 1 (January 1987), 11–14.CrossRefGoogle Scholar
  7. [7]
    Gries, D. The Science of Programming. Springer Verlag, New York, 1981.MATHGoogle Scholar
  8. [8]
    Gries, D., and J. Prins. A new notion of encapsulation. Proc. SIGPLAN 85 Symposium on Language Issues in Programming Environments. Seattle, Washington, June 1985, 131–139.CrossRefGoogle Scholar
  9. [9]
    Gries, D., and J. Prins. McLaren’s masterpiece. Science of Computer Programming 8 (1987), 139–145.CrossRefMATHGoogle Scholar
  10. [10]
    Gries, D., and J. van de Snepscheut. Inorder traversal of a binary tree and its inversion. Tech. Rpt. 87–876, Computer Science Department, Cornell University, November 1987.Google Scholar
  11. [11]
    Gries, D., and D. Volpano. The Transform -a new language construct. Structured Programming 11 (January 1990), 1–10.Google Scholar
  12. [12]
    Hoare, C.A.R. Proof of correctness of data representations. Acta Informatica 1 (1972), 271–281.CrossRefMATHGoogle Scholar
  13. [13]
    Knuth, D.E. The Art of Programming, Vol I, Fundamental Algorithms. Addison-Wesley, Reading, 1963.Google Scholar
  14. [14]
    Lutz, E. IPL.Google Scholar
  15. [15]
    Morgan, C. Data refinement by miracles. IPL 26 (1987), 243–246.CrossRefGoogle Scholar
  16. [16]
    Morgan, C., and P.H.B. Gardiner. Data refinement by calculation. Acta Informatica 27, (1990), 481–503.CrossRefMATHMathSciNetGoogle Scholar
  17. [17]
    Morris, J.M. The laws of data refinement. Ada Informatica 26(1989), 287–308.MATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • David Gries
    • 1
  1. 1.Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations