Traits: correctness-by-construction for free

DOI10.1007/978-3-031-08679-3_9zbMath1499.68067arXiv2204.05644OpenAlexW4293197076MaRDI QIDQ2165220

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

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)

Related Items (2)

Flexible Correct-by-Construction Programming ⋮ TraitCbC

Uses Software

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

Cites Work

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

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