Springer Nature is making Coronavirus research free. View research | View latest news | Sign up for updates

Proving programs correct through refinement


Program proving must be made applicable to all stages of program development. In particular, in the design phase, proving could prevent a program development based on erroneous or inconsistent design decisions, with its associated high cost of debugging. Furthermore, the proving activity itself would benefit from an early application in the development cycle of a program, because the proof of a program design seems to be simpler than the proof of the final, perhaps optimized, program. The Fisher-Galler algorithm will be used as an example for demonstrating the proof of a program design. An algebraic specification technique is used for describing the design. Details of the proof will be discussed.

This is a preview of subscription content, log in to check access.


  1. 1.

    Dijkstra, E.W.: Notes on structured programming. In: Structured programming (O.J. Dahl, E.W. Dijkstra, C.A.R. Hoare, eds.). New York: Academic Press 1972

  2. 2.

    Floyd, R.W.: Assigning meanings to programs. Proc. Symposium Applied Mathematics, AMS 19, 19–32 (1967)

  3. 3.

    Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Abstract data types as initial algebras and the correctness of data representation. Proc. Conference on computer graphics, pattern recognition, and data structure, May 1975, pp. 89–93

  4. 4.

    Guttag, J.V.: The specification and application to programming of abstract data types. University of Toronto, TR CSRG-59, September 1975

  5. 5.

    Guttag, J.V., Horowitz, E., Musser, D.R.: Abstract data types and software validation. USC ISI/RR-76–48, August 1976

  6. 6.

    Hoare, C.A.R.: Proof of correctness of data representations. Acta Informat. 1, 271–281 (1972)

  7. 7.

    Knuth, D.E.: The art of computer programming. Vol. 1. Fundamental algorithms, 2nd ed., pp. 353–355. New York: Addison-Wesley 1973

  8. 8.

    Knuth, D.E.: Structured programming with go to statements. Comput. Surveys 6, 261–301 (1974)

  9. 9.

    Liskov, B.H., Zilles, S.N.: Programming with abstract data types. In: Proc. ACM Symposium on very high level languages, SIGPLAN Notices 9.4, 50–59, April 1974

  10. 10.

    London, B.H.: A correctness proof of the Fisher-Galler algorithm using inductive assertions. In: Formal semantics of programming languages (R. Rustin, ed.). London: Prentice-Hall 1972

  11. 11.

    Morris, J.H.: A correctnesss proof using recursively defined functions. In: Formal semantics of programming languages (R. Rustin, ed.). London: Prentice-Hall 1972

  12. 12.

    Parnas, D.L.: A technique for software module specification with examples. Comm. ACM 15, 330–336 (1972)

  13. 13.

    Robinson, L., Levitt, K.N.: Proof techniques for hierarchically structured programs. Stanford Research Institute, January 1975

  14. 14.

    Spitzen, J.M., Levitt, K.L., Robinson, L.: An example of hierarchical design and proof. Stanford Research Institute, January 1976

  15. 15.

    Standish, T.A., Harriman, D.C., Kibler, D.F., Neighbors, J.M.: The Irvine program transformation catalogue. Dept. of Information and Computer Science, University of California at Irvine, January 1976

  16. 16.

    Wirth, N.: Program development by stepwise refinement. Comm. ACM 14, 221–227 (1971)

Download references

Author information

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Correll, C.H. Proving programs correct through refinement. Acta Informatica 9, 121–132 (1978).

Download citation


  • Information System
  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory