Skip to main content
SpringerLink
Log in

Quicksort Revisited

Verifying Alternative Versions of Quicksort

  • Chapter
  • First Online:
Theory and Practice of Formal Methods

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9660))

Abstract

We verify the correctness of a recursive version of Tony Hoare’s \(\texttt {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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The sorting task can actually be defined for an array of any type that has a less-then-or-equal relation \(\le \).

  2. 2.

    The careful reader will notice that the array look-up is not always defined. Nevertheless, the assertion is well-formed, because it stands for \(\forall i \in [\texttt {top}..|\texttt {a}|).\forall j \in [0.. \texttt {pivs[}i\texttt {]}).\forall k \in [\texttt {pivs[}i\texttt {]+1..|a|}).\, \texttt {a[}j\texttt {]} < \texttt {a[pivs[}i\texttt {]]} \le \texttt {a[}k\texttt {]}\).

References

  1. Apt, K., Boer, F., Olderog, E.: Verification of Sequential and Concurrent Programs. Springer, Dordrecht (2009)

    Book  MATH  Google Scholar 

  2. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  3. Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Sivarajan, S., Wheelhouse, M., Leino, K.: Dafny Code for Variations on Quicksort. http://www.doc.ic.ac.uk/~mjw03/research/quicksort.html

  4. Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Sivarajan, S., Wheelhouse, M., Leino, K.:Apollo: An interactive Program and Proof development tool for Java and Haskell, based on Dafny (to appear)

    Google Scholar 

  5. Foley, M., Hoare, C.: Proof of a recursive program: quicksort. Comput. J. 14, 391–395 (1971)

    Article  MathSciNet  MATH  Google Scholar 

  6. de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  7. Hoare, C.: Algorithm 64: quicksort. Commun. ACM 4, 321 (1961)

    Article  Google Scholar 

  8. Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)

    Article  MATH  Google Scholar 

  9. Lamort, L.:Thinking Above the Code. https://www.youtube.com/watch?v=-4Yp3j_jk8Q

  10. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Leino, K.: Dafny: An Automatic Program Verifier for Functional Correctness. http://dafny.codeplex.com

  12. Manna, Z.: Mathematical Theory of Computation. McGraw-Hill, New York (1974)

    MATH  Google Scholar 

  13. Oracle Documentation: Arrays (Java Platform SE 7). http://docs.oracle.com/javase/7/docs/api/java/util/Arrays.html

  14. The Verification Corner - Microsoft Research. http://research.microsoft.com/en-us/projects/verificationcorner

  15. Wikipedia: Quicksort. https://en.wikipedia.org/wiki/Quicksort

  16. YouTube: Quick-sort with Hungarian (Kkllmenti legnyes) folk dance. https://www.youtube.com/watch?v=ywWBy6J5gz8

Download references

Acknowledgments

We thank Krysia Broda for showing us the recursive, non-standard version of quicksort, and the anonymous reviewers of this volume for valuable suggestions and pointers.

Razvan Certezeanu, Benjamin Egelund-Muller and Sinduran Sivarajan thank the Department of Computing at Imperial College for funding their Undergraduate Research Opportunities Programme (UROP) Placements, undertaken under Mark Wheelhouse’s supervision, which they spent working on Apollo, and this paper.

Sophia Drossopoulou thanks Microsoft Research and Judith Bishop for a research gift and her very warm hospitality at Microsoft Research, and the EU project Upscale, FP7-612985, for supporting part of this work, and for the opportunity to collaborate with Frank S. de Boer, the recipient of this Festschrift.

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College London, London, UK

    Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Muller, K. Rustan M. Leino, Sinduran Sivarajan & Mark Wheelhouse

  2. Microsoft Research Redmond, Redmond, USA

    K. Rustan M. Leino

Authors
  1. Razvan Certezeanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sophia Drossopoulou
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Benjamin Egelund-Muller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. K. Rustan M. Leino
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Sinduran Sivarajan
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Mark Wheelhouse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mark Wheelhouse .

Editor information

Editors and Affiliations

  1. Informatik 2, RWTH Aachen University Informatik 2, Aachen, Germany

    Erika Ábrahám

  2. Leiden University , Leiden, The Netherlands

    Marcello Bonsangue

  3. University of Oslo , Oslo, Norway

    Einar Broch Johnsen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Leino, K.R.M., Sivarajan, S., Wheelhouse, M. (2016). Quicksort Revisited. In: Ábrahám, E., Bonsangue, M., Johnsen, E. (eds) Theory and Practice of Formal Methods. Lecture Notes in Computer Science(), vol 9660. Springer, Cham. https://doi.org/10.1007/978-3-319-30734-3_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30734-3_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-30733-6

  • Online ISBN: 978-3-319-30734-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation