A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

Norbert Schirmer

February 29, 2008

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present the theory of Simpl, a sequential imperative programming language. We introduce its syntax, its semantics (big and small-step operational semantics) and Hoare logics for both partial as well as total correctness. We prove soundness and completeness of the Hoare logic. We integrate and automate the Hoare logic in Isabelle/HOL to obtain a practically usable verification environment for imperative programs. Simpl is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method invocation and also unbounded nondeterminism.


BSD License


February 18, 2024
License change to BSD; more canonical and versatile ML interfaces; some more derived language constructs.


Session Simpl