Semantical Analysis of Specification Logic
Robert D. Tennent · Birkhäuser Boston eBooks · 1997
The specification logic of J. C. Reynolds is a partial-correctness logic for Algol 60-like languages with procedures. It is interpreted here as an intuitionistic theory, using a form of possible-world semantics first applied to programming-language interpretation by Reynolds and F. J. Oles to give an abstract treatment of stack-oriented storage management. The model provides a satisfactory solution to all previously-known problems with the interpretation of specification logic; however, unexpected new problems have been discovered in doing this work, and these remain unsolved. 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.