Hoare Logic and Auxiliary Variables |
| |
Authors: | Thomas Kleymann |
| |
Affiliation: | (1) Laboratory for Foundations of Computer Science, The University of Edinburgh, Scotland, GB |
| |
Abstract: | Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables
in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We
stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions.
Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible
for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one
can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation
in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the
presentation for verification calculi dealing with more interesting features such as recursion.
Received October 1998 / Accepted in revised form October 1999 |
| |
Keywords: | : Hoare Logic Auxiliary variables Adaptation Completeness Most General Formula VDM |
本文献已被 SpringerLink 等数据库收录! |
|