c©Wolfgang Schreiner This work is licensed under the Creative Commons Attribution License. Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs∗

We present an approach to program reasoning which inserts between a program and its verification conditions an additional layer, the denotation of the program expressed in a declarative form. The program is first translated into its denotation from which subsequently the verification conditions are generated. However, even before (and independently of) any verification attempt, one may inves-tigate the denotation itself to get insight into the “semantic essence ” of the program, in particular to see whether the denotation indeed gives reason to believe that the program has the expected be-havior. Errors in the program and in the meta-information may thus be detected and fixed prior to actually performing the formal verification. More concretely, following the relational approach to program semantics, we model the effect of a program as a binary relation on program states. A for-mal calculus is devised to derive from a program a logic formula that describes this relation and is subject for inspection and manipulation. We have implemented this idea in a comprehensive form in the RISC ProgramExplorer, a new program reasoning environment for educational purposes which encompasses the previously developed RISC ProofNavigator as an interactive proving assistant.