Traits for Correct-by-Construction Programming

TL;DR

This paper introduces TraitCbC, a trait-based approach to correctness-by-construction programming that simplifies incremental program development and verification by enabling trait composition instead of traditional refinement rules.

Contribution

It proposes TraitCbC, a novel trait-based method for correctness-by-construction, formalizes it, proves its soundness, and demonstrates a proof of concept implementation.

Findings

TraitCbC enables flexible, incremental program construction using trait composition.

The approach guarantees correctness through formal verification.

Implementation shows practical feasibility of trait-based CbC.

Abstract

We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (PhV). With Correctness-by-Construction, programs are constructed incrementally along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of refinement rules of fixed granularity which are additional rules on top of the programming language. In this work, we propose TraitCbC, an incremental program construction procedure that implements correctness-by-construction on the basis of PhV by using traits. TraitCbC enables program construction by trait composition instead of refinement rules. It provides a programming guideline, which similar to CbC should lead to well-structured programs, and allows flexible reuse of verified program building blocks. We introduce TraitCbC formally and prove the soundness of our verification strategy. Additionally, we implement TraitCbC as a proof of concept.