@inproceedings{RISC4360,author = {Wolfgang Schreiner},
title = {{Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs (Extended Abstract)}},
booktitle = {{THedu'11, CTP Components for Educational Software, Workshop associated to CADE-23}},
language = {english},
abstract = {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
investigate 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 behavior. 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 formal calculus is devised to derive from a program a 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.},
series = {CISUC Technical Report },
number = {2011/001},
pages = {55--59},
address = {Wroclaw, Poland, July 31},
isbn_issn = {ISSN 0874-338X},
year = {2011},
editor = {Pedro Quaresma and Ralph-Johan Back},
refereed = {yes},
organization = {Center for Informatics and Systems, University of Coimbra, Portugal},
length = {5}
}