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

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

3 Citaties (Scopus)

Uittreksel

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.

TaalEngels
TitelLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings
UitgeverijSpringer
Pagina's766-783
Aantal pagina's18
ISBN van geprinte versie9783319471655
DOI's
StatusGepubliceerd - 2016
Evenement7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) - Imperial, Corfu, Griekenland
Duur: 10 okt 201614 okt 2016
Congresnummer: 7

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9952 LNCS
ISSN van geprinte versie03029743
ISSN van elektronische versie16113349

Congres

Congres7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)
Verkorte titelISoLA 2016
LandGriekenland
StadImperial, Corfu
Periode10/10/1614/10/16

Vingerafdruk

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

Citeer dit

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 (blz. 766-783). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9952 LNCS). Springer. DOI: 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. blz. 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, blz. 766-783, Imperial, Corfu, Griekenland, 10/10/16. DOI: 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. blz. 766-783 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9952 LNCS).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer 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

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. blz. 766-783. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Beschikbaar vanaf, DOI: 10.1007/978-3-319-47166-2_54