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

Available as Postscript (332 KB) or compressed Postscript (123 KB).
 

PVS specification files:

semantics.dmp or compressed semantics.dmp.gz requires fixpoints.dmp or compressed fixpoints.dmp.gz

To unpack the theories type M-x undump-pvs-files in PVS. The top-level theory is simple_program.pvs.

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.

@TechReport{PDvHR96,
  author = "H. Pfeifer and A. Dold and F. W. v. Henke and H. Rue{\ss}",
  title = "{Mechanized Semantics of Simple Imperative Programming Constructs}",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "1996",
  number =       "96-11",
  type = "Ulmer Informatik-Berichte"
}