## In-Place Refinement for Effect Checking

paper ps
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#.

### Citation

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

### BibTex Entry

@inproceedings{KuncakLeino03InPlaceRefinementEffectChecking,
author = {Viktor Kuncak and Rustan Leino},
title = {In-Place Refinement for Effect Checking},
booktitle = {Workshop on Automated Verification of
Infinite-State Systems},
year = 2003,
month = {April},
abstract = {
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, {\em 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\#.
}
}