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.
Proceedings of the 11th ACM SIGPLAN International Workshop on Tools for Automatic Program Analysis
