@techreport{RISC3473,author = {Wolfgang Schreiner},
title = {{A Program Calculus}},
language = {english},
abstract = {This document describes a theory of imperative programs, i.e.\ programs that
operate on a system state which is modified by their execution.
For this purpose, we define the syntax and formal semantcs of a small
imperative programming language, introduce judgements for reasoning about
programs written in this language, and define rules for deriving true
judgements. Our treatment includes variable scopes, control flow
interruptions, and (also recursive) methods whose contracts are specified in
the style of behavioral interface description languages by preconditions,
postconditions, and frame conditions. All reasoning is modular, i.e.\ based on
the contracts of methods rather than their implementations.
The core of the calculus on the translation of commands to logical formulas
describing the state transitions allowed by the commands; this translation
thus removes the ``syntactic disguise'' of a command and discloses its
``semantic essence''. The calculus supports reasoning about a program's
well-formedness, partial correctness, and termination, as well as the
automated construction of preconditions, postconditions, and assertions.},
address = {Johannes Kepler University, Linz, Austria},
year = {2008},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC)},
length = {113}
}