Quicksort Revisited: Verifying Alternative Versions of Quicksort
File(s)quicksort.pdf (379.21 KB)
Accepted version
Author(s)
Type
Chapter
Abstract
We verify the correctness of a recursive version of Tony Hoare’s 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.
Date Issued
2016-03-13
Citation
Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer
on the Occasion of His 60th Birthday, 2016, 9660, pp.407-426
on the Occasion of His 60th Birthday, 2016, 9660, pp.407-426
ISBN
9783319307336
Publisher
Springer International Publishing
Start Page
407
End Page
426
Journal / Book Title
Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer
on the Occasion of His 60th Birthday
on the Occasion of His 60th Birthday
Lecture Notes in Computer Science
Volume
9660
Copyright Statement
© Springer Verlag 2016. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-30734-3_27
Subjects
Artificial Intelligence & Image Processing
08 Information And Computing Sciences
Publication Status
Published