Efficient substitution in hoare logic expressions

Andrew Wilson Appel, Kedar N. Swadi, Roberto Virga

Research output: Contribution to journalConference article

4 Scopus citations

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 languageEnglish (US)
Pages (from-to)35-49
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume41
Issue number3
DOIs
StatePublished - Nov 1 2001
EventHOOTS 2000, 4th International Workshop on Higher Order Operational Techniques in Semantics (Satellite to PLI 2000) - Montreal, Canada
Duration: Sep 22 2000Sep 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