Dijkstra's interpretation of the approach to solving a problem of program correctness
DOI:
https://doi.org/10.2298/YJOR1002229MKeywords:
Dijkstra, denotative interpretation, predicate, terminate, operator.Abstract
Proving the program correctness and designing the correct programs are two connected theoretical problems, which are of great practical importance. The first is solved within program analysis, and the second one in program synthesis, although intertwining of these two processes is often due to connection between the analysis and synthesis of programs. Nevertheless, having in mind the automated methods of proving correctness and methods of automatic program synthesis, the difference is easy to tell. This paper presents denotative interpretation of programming calculation explaining semantics by formulae φ and ψ, in such a way that they can be used for defining state sets for program P.References
Floyd, R.W., ”Assigning meanings to programs”, In: Proc. Sym. in Applied Math., Mathematical Aspects of Computer Science, American Mathematical Society, 19, 1980, 19-32.
Hoare, C.A.R., “An axiomatic basis for computer programming”, Communications of the ACM, 12 (1980) 576-583.
Hoare, C.A.R., “Notes on data structuring” In: Dahl, Dijkstra, Hoare Structured programming, Academic Press, (1980) 83-174.
Hoare, C.A.R., and Wirth, N., “An axiomatic definition of the programming language Pascal”, Acta Informatica, 2, 1983, 335-355.
Manna, Z., “The correctness of programs”, Journal of Computer and System Science, 3 (2) 1979.
Dijkstra, E.W., A Discipline of Programming, Prentice –Hall, 1993.
Paul, C., and Jorgensen, Software Testing, CRC Press, 1995.
Dijkstra, E.W., A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997.
Sands, D., “Total correctness by local improvement in program transformation”, Proceedings of the 22nd ACM SIGPLAN –SIGAST symposium on Principles of programming languages, S. Francisco, California, United States, 1995.
De Boer, F.S., Gabbrielli, and Meo, M.C., “A timed concurrent constraint language”, Information and Computation, August 25, 2000.
Valencia, F.D., “Reactive constraint programming”, Tech. rep., Centre for Basic Research in Computer Science (BRICS), Denmark, 2000.
Lacey, D., Jones, D.N., Wyk, E.V., and Frederiksen, C.C., “Proving correctness of compiler optimizations by temporal logic”, Proceedings of the 29th ACM SIGPLAN –SIGAST Symposium on Principles of programming languages, Portland, United States, 2002.
Harrison-Gegg, T.S., Buce, G.R., Ganetyky, D., Rebecca, Olson, C.M., and Wilson, J.D., “Studying program correctness”, Proceedings of the 8th Annual Conference on Innovation and Technology in Computer Science Education, Thessaloniki, Greece, 2003.
Scott, E., Zadirov, A., Feinberg, S., and Jayakody, R., Proceedings of Informing Science Educational Technology Education Joint Conference, Pori, Finland, 2003.
Downloads
Published
Issue
Section
License
Copyright (c) 2010 YUJOR
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
