Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs

TL;DR

This paper introduces a relational semantics-based approach to program reasoning, allowing inspection of program denotations to detect errors and understand behavior before formal verification, implemented in the RISC ProgramExplorer tool.

Contribution

It presents a novel method for analyzing program semantics through relational models, enabling pre-verification insight and error detection, integrated into an educational reasoning environment.

Findings

Effective detection of program errors prior to verification

Insight into program semantics through relational models

Implementation in the RISC ProgramExplorer tool

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 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.