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

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

doi:10.1007/978-3-319-47166-2_54

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

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

Software Engineering and Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

4 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 language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings
Publisher	Springer
Pages	766-783
Number of pages	18
ISBN (Print)	9783319471655
DOIs	https://doi.org/10.1007/978-3-319-47166-2_54
Publication status	Published - 2016
Event	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) - Imperial, Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9952 LNCS
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)
Abbreviated title	ISoLA 2016
Country/Territory	Greece
City	Imperial, Corfu
Period	10/10/16 → 14/10/16

Access to Document

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

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. et al. / 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",

note = "7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

}

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. et al.
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 proceeding › Conference contribution › Academic › peer-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.

N1 - Conference code: 7

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 - https://www.scopus.com/pages/publications/84993945089

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

T2 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)

Y2 - 10 October 2016 through 14 October 2016

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)). doi: 10.1007/978-3-319-47166-2_54

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this