Scaling Correctness-by-Construction

Abstract

The correctness-by-construction paradigm allows developers to derive formally correct programs from a pair of first-order precondition and postcondition. Although tool support has been proposed recently, and thus correctness-by-construction has left the period of pen-and-paper proofs, it is still applied in an unstructured manner to independent algorithmic problems only. To scale correctness-by-construction to more complex programs and to establish a repository of reusable off-the-shelf components, we present a formal framework and open-source tool support called ArchiCorC. In ArchiCorC, a developer models UML-style software components comprising required and provided interfaces, where methods contained in interfaces are associated to specification contracts and mapped to correct-by-construction implementations. We describe our proposed mathematical model for the horizontal and vertical composition of correct-by-construction components, and identify properties that allow to reuse them across different projects. Finally, we demonstrate feasibility of our approach on a case study and discuss future research directions related to the integration of correct-by-construction components into software engineering practices.