Sound Notional Machines
Igor Moreno Santos, Matthias Hauswirth, Johan T. Jeuring · 2024
A notional machine is a pedagogical device that abstracts away details of the semantics of a programming language to focus on some aspects of interest. A notional machine should be sound: it should be consistent with the corresponding programming language, and it should be a proper abstraction. This reduces the risk of it introducing misconceptions in education. Despite being widely used in computer science education, notional machines are usually not evaluated with respect to their soundness. To address this problem, we first introduce a formal definition of soundness for notional machines. The definition is based on the construction of a commutative diagram that relates the notional machine with the aspect of the programming language under its focus. Derived from this formalism, we present a methodology for constructing sound notional machines, which we demonstrate by applying it to a series of small case studies. We also show how the same formalism can be used to analyze existing notional machines and find inconsistencies in them as well as propose solutions to these inconsistencies. The work establishes a firmer ground for research in notional machines by serving as a framework to reason about them.