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 |