Scholars in many disciplines envy physics and its mathematical formalism, where natural processes can be described by precise equations and equational reasoning can derive consequences and yield insights that would be hard to obtain by intuition alone. This is also true for computer scientists who aim to elaborate formal calculi for describing the behavior of programs in order to get a better understanding of their properties.

In pursuit of this goal, the paper presents a set of calculational semantics that allow equational reasoning on programs. The core problem is that programs process discrete objects (computer stores) in a way that can only be adequately described by a logic with quantifiers. To support equational reasoning on such formulas, the author introduces a functional predicate calculus, where logical formulas are represented by Boolean functions and logical equivalence becomes function equality. It is shown how program behavior can be described by equations and how the laws of various other approaches to program semantics can be derived by formal calculations.

This approach has various elder relatives. For instance, the late Dijkstra, a pioneer in the field of programming theory, together with Scholten, propagated an equational style of program reasoning, and Hoare and Jifeng introduced an algebra of programming based on a view of programs as relations between states. While the calculational semantics presented in this paper does not enter new territory, it nevertheless provides a succinct working language and a framework for linking other theories.