Viktor Kuncak and Rustan Leino. In-place refinement for effect checking. In Workshop on Automated Verification of Infinite-State Systems, April 2003.

The refinement calculus is a powerful framework for reasoning about programs, specifications, and refinement relations between programs and specifications. In this paper we introduce a new refinement calculus construct, in-place refinement. We use in-place refinement to prove the correctness of a technique for checking the refinement relation between programs and specifications. The technique is applicable whenever the specification is an idempotent predicate transformer, as is the case for most procedure effects. In-place refinement is a predicate on the current program state. A command in-place refines a specification in a given state if the effect of every execution of the command in the state is no worse then the effect of some execution of the specification in the state. We demonstrate the usefulness of the in-place refinement construct by showing the correctness of a precise technique for checking effects of commands in a computer program. The technique is precise because it takes into account the set of possible states in which each command can execute, using the information about the control-flow and expressions of conditional commands. This precision is particularly important for handling aliasing in object-oriented programs that manipulate dynamically allocated data structures. We have implemented the technique as a part of a side-effect checker for the programming language C#.

[ bib ] Back