Computer Science – Logic in Computer Science
Scientific paper
2012-02-22
EPTCS 79, 2012, pp. 124-142
Computer Science
Logic in Computer Science
In Proceedings THedu'11, arXiv:1202.4535
Scientific paper
10.4204/EPTCS.79.8
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 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.
No associations
LandOfFree
Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-414703