Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families

L. Cleophas, D.G. Kourie, V. Pieterse, I. Schaefer, B.W. Watson

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)

Abstract

Correctness-by-construction (CbC) is an approach for developing algorithms inline with rigorous correctness arguments. A high-level specification is evolved into an implementation in a sequence of small, tractable refinement steps guaranteeing the resulting implementation to be correct. CbC facilitates the design of algorithms that are more efficient and more elegant than code that is hacked into correctness. In this paper, we discuss another benefit of CbC, i.e., that it supports the deep comprehension of algorithm families. We organise the different refinements of the algorithms carried out during CbC-based design in a taxonomy. The constructed taxonomy provides a classification of the commonality and variability of the algorithm family and, hence, provides deep insights into their structural relationships. Such taxonomies together with the implementation of the algorithms as toolkits provide an excellent starting point for extractive and proactive software product line engineering.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings
PublisherSpringer
Pages766-783
Number of pages18
ISBN (Print)9783319471655
DOIs
Publication statusPublished - 2016
Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) - Imperial, Corfu, Greece
Duration: 10 Oct 201614 Oct 2016
Conference number: 7

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9952 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)
Abbreviated titleISoLA 2016
CountryGreece
CityImperial, Corfu
Period10/10/1614/10/16

Fingerprint Dive into the research topics of 'Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families'. Together they form a unique fingerprint.

Cite this