Name
Abstract | ||
|---|---|---|
Correctness-by-construction (CbC), traditionally based on weakest precondition semantics, and post-hoc verification (PhV) aspire to ensure functional correctness. We argue for a lightweight approach to CbC where lack of formal rigour increases productivity. In order to mitigate the risk of accidentally introducing errors during program construction, we propose to complement lightweight CbC with PhV. We introduce lightweight CbC by example and discuss strength and weaknesses of CbC and PhV and their combination, both conceptually and using a case study. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-47166-2_52 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Predicate transformer semantics,Rigour,Software engineering,Computer science,Correctness,Software construction,Infinite loop,Semantics,Sorting algorithm | Conference | 9952 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.36 |
References | Authors | |
10 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bruce W. Watson | 1 | 338 | 53.24 |
| Derrick G. Kourie | 2 | 1 | 0.36 |
| Ina Schaefer | 3 | 1634 | 99.16 |
| Loek Cleophas | 4 | 41 | 13.89 |