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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Belgrade
2010-01-01
|
| Series: | Yugoslav Journal of Operations Research |
| Subjects: | |
| Online Access: | http://www.doiserbia.nb.rs/img/doi/0354-0243/2010/0354-02431002229M.pdf |
| Summary: | 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. |
|---|---|
| ISSN: | 0354-0243 |