tailieunhanh - Dijkstra's interpretation of the approach to solving a problem of program correctness

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. | Yugoslav Journal of Operations Research Volume 20 (2010), Number 2, 229-236 DOI: DIJKSTRAS INTERPRETATION OF THE APPROACH TO SOLVING A PROBLEM OF PROGRAM CORRECTNESS Branko MARKOSKI Technical Faculty, "Mihajlo Pupin", University of Novi Sad, Zrenjanin, Serbia markoni@ Petar HOTOMSKI Technical Faculty "Mihajlo Pupin", University of Novi Sad, Zrenjanin, Serbia Dušan MALBAŠKI Faculty of Technical Sciences, Institute of Computing and Control, University of Novi Sad, Serbia Danilo OBRADOVIĆ Faculty of Technical Sciences, Institute of Computing and Control, University of Novi Sad, Serbia Received: June 2006 / Accepted: November 2010 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. Keywords: Dijkstra, denotative interpretation, predicate, terminate, operator. AMS Subject Classification: 03BXX 230 Markoski, B., Hotomski, P., Malbaški, D., Obradović, D., / Dijkstras Interpretation 1. INTRODUCTION We are referring to, according to [Čub,1989] the main results based on matemathical-logical approach (Floyd, Manna, Waldinger, Weisman, Ness). For each program a question of termination and correctness is presented, and for two programs – the question of their equivalence. Using directed graph, a notion of abstract (non-interpreted) program is defined. Partially interpreted program is then obtained .