Semantical Analysis of Specification Logic, 2
Peter W. O’Hearn, Robert D. Tennent · Birkhäuser Boston eBooks · 1997
The “specification logic” of J. C. Reynolds (1982) is a formal system for proving partial-correctness properties of programs in an Algol-like language with higher-order procedures. In a previous publication (Tennent, 1990), a model was presented that validates all axioms of the system except those involving non-interference formulas for procedural phrases. Following Reynolds, non-interference for procedural phrases was there defined syntactically, by induction on types.