Contract Formalisation and Modular Implementation of Domain-Specific Languages

PhD Defence by Tom Hvitved

Abstract

Enterprise resource planning (ERP) systems are comprehensive and business-critical software systems. We propose a novel software architecture for ERP systems based on domain-specific languages (DSLs) and an event-based accounting model, in contrast to the traditional use of general-purpose imperative programming languages, relational database systems, and double-entry bookkeeping. Our proposed architecture extends and generalises previous work by Henglein et al., and we demonstrate the validity of our approach by implementing a small ERP system from scratch. Underlying our practical work on ERP systems, we make independent theoretical contributions to the areas of contract formalisation and DSL implementation.

Our contributions to the area of contract formalisation are a formal model of legally binding contracts and a fundamentally new generalisation of Meyer's design-by-contract (DbC) to distributed computing. The novel feature of our legally binding contracts model is blame assignment. That is, our contract model takes into account that a breach of contract must be attributable to one or more of the contract participants. We furthermore present a DSL for specifying contracts that is amenable to run-time monitoring, and which inherits the property of blame assignment by virtue of our abstract contract model. Contracts for distributed programming bare surprisingly many similarities with legally binding contracts. We propose a fundamentally new generalisation of DbC to distributed computing that, in contrast to previous work, is based on an adversarial model of system integration.

Our contribution to the area of DSL implementation is a Haskell library for constructing data types, and functions on them, in a modular and extendable fashion. Based on Swierstra's data types à la carte, our library enables full modularity and extensibility, as well as seamless support for abstract syntax tree (AST) annotations and run-time optimisation in the vein of deforestation. Additionally, we present a new approach to representing variable binders in ASTs based on Chlipala's parametric higher-order abstract syntax, while maintaining modularity and extensibility. We use our library in the implementation of our ERP architecture; not only do we benefit from the modularity in the implementation of each DSL, we also benefit from the modularity across the DSLs.


Assessment committee:

Chairman: Associate Professor Torben Ægidius Mogensen, Department of Computer Science, University of Copenhagen, Denmark

Dr. Nobuko Yoshida, Department of Computing, Imperial College, London, United Kingdom

Professor Graham Hutton, University of Nottingham, United Kingdom

Academic supervisors:

Professor Fritz Henglein, Department of Computer Science, University of Copenhagen, Denmark

Associate Professor Andrzej Filinski, Department of Computer Science, University of Copenhagen, Denmark


For an electronic copy of the thesis, please contact Jette Giovanni Møller, jettegm@diku.dk