More Web Proxy on the site http://driver.im/

research-article

An Assertional Proof of the Stability and Correctness of Natural Mergesort

Authors:

K. Rustan M. Leino,

Paqui LucioAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 17, Issue 1

Article No.: 6, Pages 1 - 22

https://doi.org/10.1145/2814571

Published: 06 November 2015 Publication History

Abstract

We present a mechanically verified implementation of the sorting algorithm Natural Mergesort that consists of a few methods specified by their contracts of pre/post conditions. Methods are annotated with assertions that allow the automatic verification of the contract satisfaction. This program-proof is made using the state-of-the-art verifier Dafny. We verify not only the standard sortedness property, but also that the algorithm performs a stable sort. Throughout the article, we provide and explain the complete text of the program-proof.

References

[1]

Roland Backhouse. 1995. The calculational method. Information Processing Letter 53, 3, 121.

[2]

Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005 (LNCS), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.), Vol. 4111. Springer, 364--387.

Digital Library

[3]

Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter. 2011. Specification and verification: The spec# experience. Communications of the ACM 54, 6 (June 2011), 81--91.

Digital Library

[4]

Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. 2013. Secure Information Flow for Java. A Dynamic Logic Approach. Extended Version. Karlsruhe reports in informatics. Fakultät für Informatik.

[5]

Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt. 2007. Verification of Object-oriented Software: The KeY Approach. Springer.

Digital Library

[6]

Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer.

Digital Library

[7]

Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009 (LNCS), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 23--42.

Digital Library

[8]

Stijn de Gouw, Frank S. de Boer, and Jurriaan Rot. 2014. Proof pearl: The key to correct and stable sorting. Journal of Automated Reasoning 53, 2, 129--139.

Digital Library

[9]

Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, and Reiner Hähnle. 2015. OpenJDK’s java.utils.Collection.sort() is broken: The good, the bad and the worst case. In Computer Aided Verification. 27th International Conference, CAV 2015 (LNCS). Springer.

[10]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008 (LNCS), C. R. Ramakrishnan and Jakob Rehof (Eds.), Vol. 4963. Springer, 337--340.

Digital Library

[11]

Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 — Where programs meet provers. In Programming Languages and Systems. 22nd European Symposium on Programming, ESOP 2013 (LNCS), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 125--128.

Digital Library

[12]

Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers.

Digital Library

[13]

Donald E. Knuth. 1973. The Art of Computer Programming, Vol. III: Sorting and Searching. Addison-Wesley.

Digital Library

[14]

Claire Le Goues, K. Rustan M. Leino, and Michał Moskal. 2011. The boogie verification debugger (tool paper). In Software Engineering and Formal Methods. 9th International Conference, SEFM 2011 (LNCS), Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.), Vol. 7041. Springer, 407--414.

Digital Library

[15]

K. Rustan and M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In LPAR-16 (LNCS), Edmund M. Clarke and Andrei Voronkov (Eds.), Vol. 6355. Springer, 348--370.

Digital Library

[16]

K. Rustan and M. Leino. 2012. Automating induction with an SMT solver. In Verification, Model Checking, and Abstract Interpretation. 13th International Conference, VMCAI 2012 (LNCS), Viktor Kuncak and Andrey Rybalchenko (Eds.), Vol. 7148. Springer, 315--331.

Digital Library

[17]

K. Rustan, M. Leino and Nadia Polikarpova. 2014. Verified calculations. In Verified Software: Theories, Tools, Experiments. 5th International Conference, VSTTE 2013, Revised Selected Papers (LNCS), Ernie Cohen and Andrey Rybalchenko (Eds.), Vol. 8164. Springer, 170--190.

[18]

K. Rustan M. Leino, and Valentin Wüstholz. 2014. The Dafny integrated development environment. In Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014 (EPTCS), Catherine Dubois, Dimitra Giannakopoulou, and Dominique Méry (Eds.), Vol. 149. 3--15.

[19]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer.

Digital Library

[20]

Christian Sternagel. 2013. Proof pearl: A mechanized proof of GHC’s mergesort. Journal of Automated Reasoning 51, 4, 357--370.

Digital Library

[21]

Julian Tschannen, Carlo A. Furia, Martin Nordio, and Nadia Polikarpova. 2015. Autoproof: Auto-active functional verification of object-oriented programs. In Tools and Algorithms for the Construction and Analysis of Systems. 21st International Conference, TACAS 2015 (LNCS), Christel Baier and Cesare Tinelli (Eds.), Vol. 9035. Springer, 566--580.

Digital Library

Cited By

Peña R(2019)An Assertional Proof of Red–Black Trees Using DafnyJournal of Automated Reasoning10.1007/s10817-019-09534-yOnline publication date: 3-Oct-2019
https://doi.org/10.1007/s10817-019-09534-y
Lucio P(2017)A Tutorial on Using Dafny to Construct Verified SoftwareElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.237.1237(1-19)Online publication date: 11-Jan-2017
https://doi.org/10.4204/EPTCS.237.1

Index Terms

An Assertional Proof of the Stability and Correctness of Natural Mergesort
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Developing verified programs with Dafny
HILT '12: Proceedings of the 2012 ACM conference on High integrity language technology

Reasoning about programs is a fundamental skill that every software engineer needs. This tutorial provides participants an opportunity to get hands-on experience with Dafny, a tool that can help develop this skill.

Dafny is a programming language and ...
Handling loops in bounded model checking of C programs via k-induction

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...
Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System

Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 17, Issue 1

December 2015

258 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/2830313

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 November 2015

Accepted: 01 August 2015

Revised: 01 June 2015

Received: 01 February 2015

Published in TOCL Volume 17, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Spanish Project
Basque Project

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
171
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)4

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Peña R(2019)An Assertional Proof of Red–Black Trees Using DafnyJournal of Automated Reasoning10.1007/s10817-019-09534-yOnline publication date: 3-Oct-2019
https://doi.org/10.1007/s10817-019-09534-y
Lucio P(2017)A Tutorial on Using Dafny to Construct Verified SoftwareElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.237.1237(1-19)Online publication date: 11-Jan-2017
https://doi.org/10.4204/EPTCS.237.1

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents