AlanLight
Master Project of Gerben Kunst

Abstract

For programs controlling industrial processes, it is of vital importance that they produce results conform their functional specification. Furthermore, it is important that their running times are bounded, and that we can predict corresponding worst-case scenarios. Programs written in general purpose programming languages can crash or produce erroneous output. Data modeling and query languages are typically more restrictive. However, they either do not guarantee soundness (where values are of a predefined indivisible type) or functional correctness (including deterministic output). Alternatively, they have unbounded or unpredictable worst-case running times, or have limited expressiveness.We present AlanLight, a data modeling language for expressing complex recursive calculations, while guaranteeing soundness, functional correctness, and polynomial time complexity in the size of user data. To achieve this, we use complex referential integrity constraints and an elegant, formally defined analysis over constraint and calculation definitions in AlanLight programs. Furthermore, we give a formal specification of the dynamic semantics of AlanLight, implying its guarantees, and demonstrating support for on-demand minimal effort calculation.

Thesis

• Kunst, Gerben. AlanLight. TU Delft Repository, 2018.