Efficient Substitution in Hoare Logic Expressions

Substitution plays an important role in Hoare Logic, as it is used in interpreting assignments. When writing a computer-based realization of Hoare Logic, it is therefore important to choose a good implementation for it. In this paper we compare different definitions and implementations of substitution in a logical framework, in an effort to maximize efficiency. We start by defining substitution as a logical formula. In a conventional approach, this is done by specifying the syntactic changes substitution performs on expressions. We choose instead a semantic definition that describes the behavioral relation between the original expression and its substituted counterpart. Next, we use this semantic definition as an abstract specification, and compare two of its concrete implementations. The first we consider is the usual one, that operates recursively over the structure of the term. This requires a number of inference steps proportional to the size of the expression, which is unacceptable for many practical applications. We therefore propose a different method, that makes better use of the primitives provided by the logical framework, and manages to reduce the complexity to a quantity proportional to the number of free variables. We conclude the paper outlining a refinement technique that, by taking advantage of some simple program analysis information, holds promise of improving the results presented even further.