University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Our Papers

Guided Tour Through a Mechanized Semantics of Simple Imperative Programming Constructs

H. Pfeifer, F.W. v. Henke, H. Rueß

Revised version of Technical Report UIB 96-11
Universität Ulm, Fakultät für Informatik, July 1997


 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.

 Online Copy

Available as Postscript (269 KB) or compressed Postscript (102 KB)

PVS specification files: semantics.dmp or compressed semantics.dmp.gz
requires fixpoints.dmp or compressed fixpoints.dmp.gz

Note: 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.

 BibTeX Entry


@TechReport{PvHR97,
  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
           \url{http://www.informatik.uni-ulm.de/ki/PVS/semantics.html}},
}


Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - July 29, 1997