### Abstract

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.

Original language | English (US) |
---|---|

Pages (from-to) | 35-49 |

Number of pages | 15 |

Journal | Electronic Notes in Theoretical Computer Science |

Volume | 41 |

Issue number | 3 |

DOIs | |

State | Published - Nov 1 2001 |

Event | HOOTS 2000, 4th International Workshop on Higher Order Operational Techniques in Semantics (Satellite to PLI 2000) - Montreal, Canada Duration: Sep 22 2000 → Sep 22 2000 |

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'Efficient substitution in hoare logic expressions'. Together they form a unique fingerprint.

## Cite this

*Electronic Notes in Theoretical Computer Science*,

*41*(3), 35-49. https://doi.org/10.1016/S1571-0661(04)80872-7