×

zbMATH — the first resource for mathematics

Proof pearl: The KeY to correct and stable sorting. (English) Zbl 1314.68277
Summary: We discuss a proof of the correctness of two sorting algorithms: Counting sort and Radix sort. The semi-automated proof is formalized in the state-of-the-art theorem prover KeY.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68P10 Searching and sorting
Software:
Coq; JML; KeY; Quicksort
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ahrendt, W., Mostowski, W., Paganelli, G.: Real-time Java API specifications for high coverage test generation. In: Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES ’12, pp. 145-154. ACM, New York (2012). doi:10.1145/2388936.2388960 · Zbl 1314.68288
[2] Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd Edn. Texts in Computer Science. Springer-Verlag (2009). 502 pp, ISBN 978-1-84882-744-8 · Zbl 1183.68361
[3] Apt, KR; Boer, FS; Olderog, ER; Gouw, S, Verification of object-oriented programs: A transformational approach, J. Comput. Syst. Sci., 78, 823-852, (2012) · Zbl 1245.68062
[4] Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Secure information flow for Java. A Dynamic Logic approach. Karlsruhe reports in informatics; 2013-10, KIT (2013). http://digbib.ubka.uni-karlsruhe.de/volltexte/1000036786
[5] Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science, vol. 4334. Springer (2007) · Zbl 0231.68011
[6] Burdy, L; Cheon, Y; Cok, DR; Ernst, MD; Kiniry, JR; Leavens, GT; Leino, KRM; Poll, E, An overview of JML tools and applications, Int. J. Softw. Tools Technol. Transfer, 7, 212-232, (2005)
[7] Filliâtre, J.C., Magaud, N.: Certification of sorting algorithms in the system Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends. Nice, France (1999). http://www.lri.fr/filliatr/ftp/publis/Filliatre-Magaud.ps.gz
[8] Foley, M; Hoare, CAR, Proof of a recursive program: quicksort, Comput. J., 14, 391-395, (1971) · Zbl 0231.68011
[9] Mostowski, W.: Formalisation and verification of Java Card security properties in Dynamic Logic. In: M. Cerioli (ed.) Proceedings Fundamental Approaches to Software Engineering (FASE), Edinburgh, Lecture Notes in Computer Science, vol. 3442, pp. 357-371. Springer (2005). http://www.springerlink.com/link.asp?id=x0u5bj47bcqhy4b7 · Zbl 1119.68351
[10] Mostowski, W.: Fully verified Java Card API reference implementation. In: VERIFY (2007) · Zbl 0231.68011
[11] Sternagel, C, Proof pearl - A mechanized proof of GHC’s mergesort, J. Autom. Reasoning, 51, 357-370, (2013) · Zbl 1314.68288
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.