Idealized Algol and its Specification Logic
John Reynolds · Birkhäuser Boston eBooks · 1997
Specification logic is a new formal system for program proving that is applicable to programming languages, such as A lgol , whose procedure mechanism can be described by the copy rule. The starting point of its development is the recognition that, in the presence of an A lgol -like procedure mechanism, specifications , such as the Hoare triple { P } S { Q } [Hoare, 1969], must be regarded as predicates about environments (in the sense of Landin [Landin, 1965; Landin, 1966]). The logic provides additional kinds of specifications describing an interference relation (#) between variables and other entities, and permits specifications to be compounded using the operations of implication (⇒), conjunction (&), and universal quantification ( ∀ ). The result is a system in which one can infer universal specifications, i.e. specifications that hold in all environments. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.