Traits: correctness-by-construction for free

DOI10.1007/978-3-031-08679-3_9MaRDI QIDQ2165220zbMATH OpenOpenAlexFDO

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

Publication date 19 August 2022

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)

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.

Recommendations

• Verifying traits: an incremental proof system for fine-grained reuse
• The correctness-by-construction approach to programming
• Gradual program verification
• Trace-based verification of imperative programs with I/O
• Look for the proof to find the program: decorated-component-based program synthesis

Cites work

• ArcAngel: a tactic language for refinement
• Dafny: an automatic program verifier for functional correctness
• Data refinement in Isabelle/HOL
• Feature integration using a feature construct
• First-Class Type Classes
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 3995020 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• Invariant based programming: Basic approach and teaching experiences
• Modeling in Event B. System and software engineering.
• Refinement Calculus
• The correctness-by-construction approach to programming
• Verifying traits: an incremental proof system for fine-grained reuse

Cited in

(3)

• TraitCbC
• Flexible Correct-by-Construction Programming
• Verifying traits: an incremental proof system for fine-grained reuse

Describes a project that uses

Uses Software

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

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)