Traits: Correctness-by-Construction for Free

Simple item page
dc.contributor.authorRunge, Tobiasen
dc.contributor.authorPotanin, Alexen
dc.contributor.authorThüm, Thomasen
dc.contributor.authorSchaefer, Inaen
dc.coverage.spatialLucca, Italyen
dc.date.accessioned2026-03-01T17:43:30Z
dc.date.available2026-03-01T17:43:30Z
dc.date.issued2022-06-12en
dc.description.abstractWe 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.en
dc.description.statusPeer-revieweden
dc.format.extent20en
dc.identifier.isbn978-3-031-08678-6en
dc.identifier.isbn978-3-031-08679-3en
dc.identifier.issn0302-9743en
dc.identifier.otherdblp:conf/forte/RungePTS22en
dc.identifier.otherORCID:/0000-0002-4242-2725/work/206894449en
dc.identifier.scopus85132975396en
dc.identifier.urihttps://hdl.handle.net/1885/733806865
dc.language.isoenen
dc.publisherSpringer Science+Business Media B.V.en
dc.relation.ispartofFormal Techniques for Distributed Objects, Components, and Systems - 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedingsen
dc.relation.ispartofseries42nd IFIPWG6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022en
dc.relation.ispartofseriesLecture Notes in Computer Scienceen
dc.rightsPublisher Copyright: © 2022, IFIP International Federation for Information Processing.en
dc.titleTraits: Correctness-by-Construction for Freeen
dc.typeConference paperen
dspace.entity.typePublicationen
local.bibliographicCitation.lastpage150en
local.bibliographicCitation.startpage131en
local.contributor.affiliationRunge, Tobias; Technical University of Braunschweigen
local.contributor.affiliationPotanin, Alex; School of Computing, ANU College of Systems and Society, The Australian National Universityen
local.contributor.affiliationThüm, Thomas; Ulm Universityen
local.contributor.affiliationSchaefer, Ina; Technical University of Braunschweigen
local.identifier.ariespublicationa383154xPUB37023en
local.identifier.doi10.1007/978-3-031-08679-3_9en
local.identifier.essn1611-3349en
local.identifier.pure4c85036f-6900-4175-94d8-a689a525657ben
local.identifier.urlhttps://www.scopus.com/pages/publications/85132975396en
local.type.statusPublisheden

Downloads

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS