Correctness-by-Construction in Stringology
| Abstract: |
| Correctness-by-construction (CbC) is an algorithm derivation technique in which the algorithm is co-developed with its correctness proof. Starting with a specification (most often as a pre- and post-condition), `derivation steps' are made towards a final algorithm. Critically, each step in the derivation is a correctness-preserving one, meaning that the composition of the derivation steps is the correctness proof. |
| Download paper: | ![]() |
![]() |
![]() |
| PostScript | BibTeX reference |