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.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
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
Floyd, R.W.: Assigning meanings to programs. Proc. Symposium Applied Mathematics, AMS 19, 19–32 (1967)
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
Guttag, J.V.: The specification and application to programming of abstract data types. University of Toronto, TR CSRG-59, September 1975
Guttag, J.V., Horowitz, E., Musser, D.R.: Abstract data types and software validation. USC ISI/RR-76–48, August 1976
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informat. 1, 271–281 (1972)
Knuth, D.E.: The art of computer programming. Vol. 1. Fundamental algorithms, 2nd ed., pp. 353–355. New York: Addison-Wesley 1973
Knuth, D.E.: Structured programming with go to statements. Comput. Surveys 6, 261–301 (1974)
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
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
Morris, J.H.: A correctnesss proof using recursively defined functions. In: Formal semantics of programming languages (R. Rustin, ed.). London: Prentice-Hall 1972
Parnas, D.L.: A technique for software module specification with examples. Comm. ACM 15, 330–336 (1972)
Robinson, L., Levitt, K.N.: Proof techniques for hierarchically structured programs. Stanford Research Institute, January 1975
Spitzen, J.M., Levitt, K.L., Robinson, L.: An example of hierarchical design and proof. Stanford Research Institute, January 1976
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
Wirth, N.: Program development by stepwise refinement. Comm. ACM 14, 221–227 (1971)
About this article
Cite this article
Correll, C.H. Proving programs correct through refinement. Acta Informatica 9, 121–132 (1978). https://doi.org/10.1007/BF00289073
- Information System
- Operating System
- Data Structure
- Communication Network
- Information Theory