Thursday, 28 April 2016, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: A wide class of formal specs is of the form: "Please preserve this part of the input, otherwise feel free to optimize it according to (...)". In program refactoring, for instance, a given piece of source code can be shaped up to best coding practices provided its meaning does not change.
This talk introduces "metaphors" and their algebra to reason about such specs and, in particular, to derive (functional) code from them. A particular kind of refinement is addressed capturing a strategy known as "change of virtual data structure".
This will be illustrated with the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.