Аннотация:
For the most part, inventing a new algorithm is equal parts deep insight, experience, luck, and creativity. In this talk, I will introduce a more systematic approach to inventive algorithmics — an approach which also provides a correctness argument.
Correctness-by-construction (CbC) is an algorithm derivation technique in which the algorithm is co-developed with its correctness proof. Starting with a pre- and post-condition specification, ‘derivation steps’ are made, eventually arriving at the 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. While CbC can be used for already-invented algorithms, it can be used for taxonomization and also for identifying openings for new algorithms. This will be demonstrated on string, tree and FCA algorithms.
Обратная связь: