PhD Dissertation Defence of Igor Moreno Santos
Sound Notional Machines
USI, Lugano, Switzerland
Thu, Sep 28, 2023
Abstract
A notional machine is a pedagogic 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. Notional machines found in the computer science education literature 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 and the aspect of the programming language the notional machine is focused on. Leveraging this formalism, we present a methodology for constructing sound notional machines and a similar methodology to reveal potential inconsistencies in existing notional machines. We apply these methodologies to build sound-by-construction notional machines and find inconsistencies in existing ones as well as propose solutions to these inconsistencies. Finally, we show that the same commutative diagram that describes a notional machine can be used also to design experiments to evaluate that notional machine as an educational assessment instrument.