Proof Pearl: The KeY to Correct and Stable Sorting

详细信息    查看全文

• 作者：Stijn de Gouw (1) (2)
  Frank de Boer (1) (2)
  Jurriaan Rot (1) (2)
  
• 关键词：Sorting ; Correctness ; Theorem prover ; KeY ; Counting sort ; Radix sort
• 刊名：Journal of Automated Reasoning
• 出版年：2014
• 出版时间：August 2014
• 年：2014
• 卷：53
• 期：2
• 页码：129-139
• 全文大小：299 KB
• 参考文献：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 鈥?2, pp. 145鈥?54. ACM, New York (2012). doi:10.1145/2388936.2388960
  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
  3. Apt, K.R., de Boer, F.S., Olderog, E.R., de Gouw, S.: Verification of Object-Oriented programs: A transformational approach. J. Comput. Syst. Sci. 78(3), 823鈥?52 (2012) CrossRef
  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)
  6. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transfer 7(3), 212鈥?32 (2005) CrossRef
  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, C.A.R.: Proof of a recursive program: Quicksort. Comput. J. 14(4), 391鈥?95 (1971) CrossRef
  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鈥?71. Springer (2005). http://www.springerlink.com/link.asp?id=x0u5bj47bcqhy4b7
  10. Mostowski, W.: Fully verified Java Card API reference implementation. In: VERIFY (2007)
  11. Sternagel, C.: Proof Pearl - A mechanized proof of GHC鈥檚 mergesort. J. Autom. Reasoning 51(4), 357鈥?70 (2013) CrossRef
  
• 作者单位：Stijn de Gouw (1) (2)
  Frank de Boer (1) (2)
  Jurriaan Rot (1) (2)
  
  1. LIACS 鈥?Leiden University, Leiden, Netherlands
  2. CWI, Amsterdam, Netherlands
  
• ISSN：1573-0670

文摘

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.