Traits: correctness-by-construction for free

DOI10.1007/978-3-031-08679-3_9zbMATH Open1499.68067arXiv2204.05644OpenAlexW4293197076MaRDI QIDQ2165220FDOQ2165220

Thomas Thüm, Alex Potanin, Ina Schaefer, Tobias Runge

Publication date: 19 August 2022

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.

Full work available at URL: https://arxiv.org/abs/2204.05644

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Dafny: An Automatic Program Verifier for Functional Correctness
• ArcAngel: a tactic language for refinement
• Refinement Calculus
• Invariant based programming: Basic approach and teaching experiences
• Verifying traits: an incremental proof system for fine-grained reuse
• Data Refinement in Isabelle/HOL
• Feature integration using a feature construct
• First-Class Type Classes
• The Correctness-by-Construction Approach to Programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (2)

• TraitCbC
• Flexible Correct-by-Construction Programming

Uses Software

• Dafny
• ArcAngel
• Eiffel
• JML
• Spec#
• Rodin
• VCC
• VeriFast
• Featherweight Java
• AutoProof
• TraitRecordJ

This page was built for publication: Traits: correctness-by-construction for free

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2165220)