Machine-Checked Correctness and Complexity of a Union-Find Implementation

Опубликовано 13 июня 2016, 20:14

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. Using Coq and the CFML tool, Arthur Chargu'raud and I have verified the correctness and amortized complexity of an OCaml implementation of Union-Find. In this talk, I will give an overview of our approach, which uses higher-order separation logic extended with time credits. This approach allows us to state (and establish) a single specification that covers correctness and complexity at the same time.