Guided Tour Through a Mechanized Semantics of Simple Imperative Programming Constructs

Revised Version of UIB-96-11as of July 1997.

---

Authors

Holger Pfeifer and F.W. von Henke and Harald Rueß

Abstract

In this paper a uniform formalization in PVS of various kinds of semantics of imperative programming language constructs is presented. Based on a comprehensive development of fixed point theory, the denotational semantics of elementary constructs of imperative programming languages are defined as state transformers. These state transformers induce corresponding predicate transformers, providing a means to formally derive both a weakest liberal precondition semantics and an axiomatic semantics in the style of Hoare. Moreover, algebraic laws as used in refinement calculus proofs are validated at the level of predicate transformers. Simple reformulations of the state transformer semantics yield both a continuation-style semantics and rules similar to those used in structural operational semantics.

gzipped postscript or postscript

BibTeX Entry

@TechReport{PDvHR97,
  author = {F.W. v. Henke and H. Pfeifer and H. Rue{\ss}},
  title =  {Guided Tour Through a Mechanized Semantics of Simple Imperative Programming Constructs},
  institution =  {Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik},
  year    = {1997},
  number =  {96-11},
  type   = {Ulmer Informatik-Berichte},
  note = {This is a major revision of the Technical Report UIB-96-11 with the title
          "Mechanized Semantics of Simple Imperative Programming Constructs". The
	   original version can still be found at
	   \ulr{http://www.informatik.uni-ulm.de/ki/PVS/semantics.html}},
}

---

PVS theories

(these theories require an older version of the fixpoint library. The semantics specification expects the formaliziation of fixed-point theory being placed in a subdirectory called "Fixpoints". If the fixed-point library is already installed in a different directory, the LIBRARY declarations in some of the files will have to be changed accordingly.)

---

This formalization provides the foundations on which formal specification of programming languages and mechanical verification of compilation steps are carried out within the Verifix project, which is concerned with constructing provably correct compilers.

---

Harald Ruess: ruess@csl.sri.com