Quicksort Revisited - Verifying Alternative Versions of Quicksort.
Theory and Practice of Formal Methods(2016)
摘要
We verify the correctness of a recursive version of Tony Hoare's $\texttt {quicksort}$quicksort algorithm using the Hoare-logic based verification tool Dafny. We then develop a non-standard, iterative version which is based on a stack of pivot-locations rather than the standard stack of ranges. We outline an incomplete Dafny proof for the latter.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络