A re-construction of the fundamentals of programming as a small mathematical theory (PRISM) based on elementary set theory. Highlights: ∙ Zero axioms. No properties are assumed, all are proved (from standard set theory). ∙ A single concept covers specifications and programs. ∙ Its definition only involves one relation and one set. ∙ Everything proceeds from three operations: choice, composition and restriction. ∙ These techniques suffice to derive the axioms of classic papers on the “laws of programming” as consequences and prove them mechanically. ∙ The ordinary subset operator suffices to define both the notion of program correctness and the concepts of specialization and refinement. ∙ From this basis, the theory deduces dozens of theorems characterizing important properties of programs and programming. ∙ All these theorems have been mechanically verified (using Isabelle/HOL); the proofs are available in a public repository. This paper is a considerable extension and rewrite of an earlier contribution.
Chair of Software Engineering