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
de Boer, F.S., Gabbrielli,, Meo, M.C. (2000) A timed concurrent constraint language. Information and Computation, August 25
Dijkstra, E.W. (1993) A discipline of programming. Englewood Cliffs, NJ, itd: Prentice Hall
Dijkstra, E.W. (1997) A Discipline of Programming. Upper Saddle River,NJ: Prentice Hall
Floyd, R.W. (1980) Assigning meanings to programs. u: Symposium in Applied Math., Mathematical Aspects of Computer Science, Proceedings, American Mathematical Society, 19, str. 19-32
Harrison-Gegg, T.S., Buce, G.R., Ganetyky, D., Rebecca, O.C.M., Wilson, J.D. (2003) Studying program correctness. u: Proceedings of the 8th Annual Conference on Innovation and Technology in Computer Science Education, Thessalonica, Greece
Hoare, C.A. (1969) An axiomatic basis for computer programming. Communications of the ACM, 12(10): 576
Hoare, C.A., Wirth, N. (1973) An axiomatic definition of the programming language PASCAL. Acta Informatica, 2(4): 335
Hoare, C.A.R. (1980) Notes on data structuring. u: Dahl Dijkstra [ur.] Hoare Structured programming, Academic Press, str. 83-174
Lacey, D., Jones, D.N., Wyk, E.V., Frederiksen, C.C. (2002) Proving correctness of complier optimations by temporal logic. u: Proceedings of the 29th ACM SIGPLAN -SIGAST Symposium on Principles of programming languages, Portland
Manna, Z. (1969) The correctness of programs. Journal of Computer and System Sciences, 3 (2)
Paul, C., Jorgensen (1995) Software testing. CRC Press
Sands, D. (1995) Total correctness by local improvement in program transformation. u: ACM SIGPLAN -SIGAST symposium on Principles of programming languages (22), S. Francisco, Proceedings
Scott, E., Zadirov, A., Feinberg, S., Jayakody, R. (2003) u: Proceedings of Informing Science Educational Technology Education Joint Conference, Pori
Valencia, F.D. (2000) Reactive constraint programming. Denmark: Centre for Basic Research in Computer Science (Brics), Tech. rep
Downloads
Published
Issue
Section
License
Copyright (c) YUJOR
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
