A Program Calculus

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.