In-Place Refinement for Effect Checking
Viktor Kunčak, Rustan Leino · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · 2003
The re nement calculus is a powerful framework for reasoning about programs, speci cations, and re nement relations between programs and speci cations.In this paper we introduce a new re nement calculus construct, in-place re nement.We use in-place re nement to prove the correctness of a technique for checking the re nement relation between programs and speci cations.The technique is applicable whenever the speci cation is an idempotent predicate transformer, as is the case for most procedure effects.In-place re nement is a predicate on the current program state.A command in-place re nes a speci cation in a given state if the eect of every execution of the command in the state is no worse then the eect of some execution of the speci cation in the state.We demonstrate the usefulness of the in-place re nement construct by showing the correctness of a precise technique for checking eects 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-ow 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-eect checker for the programming language C#.