AlanLight
sound, functionally correct, bounded acyclic data flow modeling
G.J. Kunst (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Daco Harkes – Mentor
C. Schraverus – Mentor
E Visser – Graduation committee member
MTJ Spaan – Graduation committee member
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
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.