Chapter 14 Semantical Analysis of Specification Logic, 2
Peter W. O’Hearn, Robert D. Tennent · 1997
The specification logic of J. C. Reynolds (1982) is a formal system for proving partial-correctness properties of programs in an ALGOL-like lan guage with higher-order procedures. In a previous publication (Tennent, 1990), a model was presented that validates all axioms of the system ex cept those involving non-interference formulas for procedural phrases. Following Reynolds, non-interference for procedural phrases was there defined syntactica/ly, by induction on types. Here, we present a new semantic interpretation of non-interference (for phrases of arbitrary type) which is equivalent to the interpretation given earlier for phrases of basic type. This interpretation provides the first model for a/1 of Reynolds's axioms (except the equivalences formerly used to define procedural non-interference). A slightly more refined model is used to validate also a new axiom which formalizes a method used by Reynolds (1981a) to reason about programs with multiple Ievels of abstraction.