Reuse of Invariants in Proofs of Implementation

Abstract

In this paper we describe a technique to inherit safety properties from abstract programs to their implementations. With this technique repetition of many proofs can be avoided.

Let P be a concurrent program and P' its implementation. The basic idea is taken from L. Lamport: establish a map alpha from the state space of P' to the state space of P, and map all reachable atomic transitions (s', t') of P' to pairs of states, (alpha(s'),alpha(t')), in the state space of P; if each pair can be demonstrated to be either an atomic transition of P or the empty transition, alpha(s') = alpha(t') , then any safety property of P invariant to arbitrary repetition of states induce a similar safety property of P'.

For many programs some of the unreachable transitions in P' do not map this way; hence it may be necessary to characterise the reachable states of P' in advance of the above demonstration. We prove that the properties we want to inherit can safely be used for this. The main purpose of the paper is to demonstrate the utility of such a result.

The theoretical results in the paper are worked out into gradually more powerful techniques for inheriting safety properties. These proof techniques are illustrated with examples.