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

Taxonomies
Taxonomy
Correctness
Refinement
Design of Algorithms
Software Product Lines
Family
Specification
Engineering
Specifications

Cite this

Cleophas, L., Kourie, D. G., Pieterse, V., Schaefer, I., & Watson, B. W. (2016). Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings (pp. 766-783). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9952 LNCS). Springer. https://doi.org/10.1007/978-3-319-47166-2_54
Cleophas, L. ; Kourie, D.G. ; Pieterse, V. ; Schaefer, I. ; Watson, B.W. / Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Springer, 2016. pp. 766-783 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{68367dbe2826474e929c0ecfb003b5b3,
title = "Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families",
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.",
author = "L. Cleophas and D.G. Kourie and V. Pieterse and I. Schaefer and B.W. Watson",
year = "2016",
doi = "10.1007/978-3-319-47166-2_54",
language = "English",
isbn = "9783319471655",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "766--783",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings",
address = "Germany",

}

Cleophas, L, Kourie, DG, Pieterse, V, Schaefer, I & Watson, BW 2016, Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families. in Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9952 LNCS, Springer, pp. 766-783, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Imperial, Corfu, Greece, 10/10/16. https://doi.org/10.1007/978-3-319-47166-2_54

Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families. / Cleophas, L.; Kourie, D.G.; Pieterse, V.; Schaefer, I.; Watson, B.W.

Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Springer, 2016. p. 766-783 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9952 LNCS).

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

TY - GEN

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

AU - Cleophas, L.

AU - Kourie, D.G.

AU - Pieterse, V.

AU - Schaefer, I.

AU - Watson, B.W.

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84993945089&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-47166-2_54

DO - 10.1007/978-3-319-47166-2_54

M3 - Conference contribution

AN - SCOPUS:84993945089

SN - 9783319471655

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 766

EP - 783

BT - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings

PB - Springer

ER -

Cleophas L, Kourie DG, Pieterse V, Schaefer I, Watson BW. Correctness-by-construction ∧ taxonomies ⇒ deep comprehension of algorithm families. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Springer. 2016. p. 766-783. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-47166-2_54