Name
Abstract | ||
|---|---|---|
Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1007/978-3-030-16722-6_2 | FASE |
Field | DocType | Citations |
CORC,Programming language,Computer science,Correctness,Automated theorem proving,Program development,Postcondition | Conference | 0 |
PageRank | References | Authors |
0.34 | 0 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tobias Runge | 1 | 0 | 2.03 |
| Ina Schaefer | 2 | 1634 | 99.16 |
| Loek Cleophas | 3 | 41 | 13.89 |
| Thomas Thüm | 4 | 1048 | 47.15 |
| Derrick G. Kourie | 5 | 223 | 33.10 |
| Bruce W. Watson | 6 | 338 | 53.24 |