Transformational verification of Quicksort. (English) Zbl 07453193
Fribourg, Laurent (ed.) et al., Proceedings of the eighth international workshop on verification and program transformation and the seventh workshop on Horn clauses for verification and synthesis, VPT/HCVS 2020, Dublin, Ireland, April 25–26, 2020. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 320, 95-109 (2020).
Summary: Many transformation techniques developed for constraint logic programs, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work out a nontrivial case study through the transformation-based verification approach. We consider the familiar Quicksort program for sorting lists, written in a functional programming language, and we verify the pre/-postconditions that specify the intended correctness properties of the functions defined in the program. We verify these properties by: (1) translating them into CHCs, (2) transforming the CHCs by removing all list occurrences, and (3) checking the satisfiability of the transformed CHCs by using the Eldarica solver over booleans and integers. The transformation mentioned at Point (2) requires an extension of the algorithms for the elimination of inductively defined data structures presented in previous work, because during one stage of the transformation we use as lemmas some properties that have been proved at previous stages.
For the entire collection see [Zbl 1466.68013].
For the entire collection see [Zbl 1466.68013].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | E. Albert, M. Gómez-Zamalloa, L. Hubert & G. Puebla (2007): Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In M. Hanus, editor: Practical Aspects of Declarative Languages, Lecture Notes in Computer Science 4354, Springer, pp. 124-139, doi:10.1007/978-3-540-69611-7_8. · doi:10.1007/978-3-540-69611-7_8 |
| [2] | K. R. Apt, F. S. de Boer & E.-R. Olderog (2009): Verification of Sequential and Concurrent Programs, Third edition. Springer, doi:10.1007/978-1-84882-745-5. · Zbl 1183.68361 · doi:10.1007/978-1-84882-745-5 |
| [3] | G. Banda & J. P. Gallagher (2009): Analysis of Linear Hybrid Systems in CLP. In Michael Hanus, editor: Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valen-cia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science 5438, Springer, pp. 55-70, doi:10.1007/978-3-642-00515-2_5. · Zbl 1185.68406 · doi:10.1007/978-3-642-00515-2_5 |
| [4] | N. Bjørner, A. Gurfinkel, K. L. McMillan & A. Rybalchenko (2015): Horn Clause Solvers for Program Verification. In L. D. Beklemishev, A. Blass, N. Dershowitz, B. Finkbeiner & W. Schulte, editors: Fields of Logic and Computation II -Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Lecture Notes in Computer Science 9300, Springer, pp. 24-51, doi:10.1007/978-3-319-23534-9_2. · Zbl 1465.68044 · doi:10.1007/978-3-319-23534-9_2 |
| [5] | M. Bruynooghe, M. Codish, J. P. Gallagher, S. Genaim & W. Vanhoof (2007): Termination analysis of logic programs through combination of type-based norms. ACM Trans. Program. Lang. Syst. 29(2), pp. 10-es, doi:10.1145/1216374.1216378. · doi:10.1145/1216374.1216378 |
| [6] | A. Bundy (2001): The Automation of Proof by Mathematical Induction. In A. Robinson & A. Voronkov, editors: Handbook of Automated Reasoning, I, North Holland, pp. 845-911, doi:10.1016/ B978-044450813-3/50015-1. · Zbl 0994.03007 · doi:10.1016/B978-044450813-3/50015-1 |
| [7] | R. M. Burstall & J. Darlington (1977): A Transformation System for Developing Recursive Programs. Journal of the ACM 24(1), pp. 44-67, doi:10.1145/321992.321996. · Zbl 0343.68014 · doi:10.1145/321992.321996 |
| [8] | R. Certezeanu, S. Drossopoulou, B. Egelund-Müller, K. R. M. Leino, S. Sivarajan & M. J. Wheelhouse (2016): Quicksort Revisited -Verifying Alternative Versions of Quicksort. In E.Ábrahám, M. M. Bonsangue & E. Broch Johnsen, editors: Theory and Practice of Formal Methods -Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 9660, Springer, pp. 407-426, doi:10. 1007/978-3-319-30734-3_27. · Zbl 1475.68102 · doi:10.1007/978-3-319-30734-3_27 |
| [9] | E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): Program Verification via Iterated Special-ization. Science of Computer Programming 95, Part 2, pp. 149-175, doi:10.1016/j.scico.2014.05. 017. · doi:10.1016/j.scico.2014.05.017 |
| [10] | E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): VeriMAP: A Tool for Verifying Pro-grams through Transformations. In: Proceedings of the 20th International Conference on Tools and Al-gorithms for the Construction and Analysis of Systems, TACAS ’14, Lecture Notes in Computer Science 8413, Springer, pp. 568-574, doi:10.1007/978-3-642-54862-8_47. Available at http://www.map. uniroma2.it/VeriMAP. · doi:10.1007/978-3-642-54862-8_47 |
| [11] | E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2017): Semantics-based generation of verification conditions via program specialization. Science of Computer Programming 147, pp. 78-108, doi:10.1016/ j.scico.2016.11.002. · doi:10.1016/j.scico.2016.11.002 |
| [12] | E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018): Solving Horn Clauses on Inductive Data Types Without Induction. Theory and Practice of Logic Programming 18(3-4), pp. 452-469, doi:10.1017/ S1471068418000157. Special Issue on ICLP ’18. · Zbl 1451.68172 · doi:10.1017/S1471068418000157 |
| [13] | E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2020): Removing Algebraic Data Types from Con-strained Horn Clauses Using Difference Predicates. In: Proceedings of the International Joint Conference on Automated Reasoning, IJCAR ’20, Lecture Notes in Computer Science 12166, Springer, Cham, pp. 83-102, doi:10.1007/978-3-030-51074-9_6. · Zbl 07614508 · doi:10.1007/978-3-030-51074-9_6 |
| [14] | G. Delzanno & A. Podelski (1999): Model Checking in CLP. In R. Cleaveland, editor: 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’99, Lecture Notes in Computer Science 1579, Springer-Verlag, pp. 223-239, doi:10.1007/3-540-49059-0_16. · doi:10.1007/3-540-49059-0_16 |
| [15] | S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101-146, doi:10.1016/0304-3975(95)00148-4. · Zbl 0872.68021 · doi:10.1016/0304-3975(95)00148-4 |
| [16] | F. Fioravanti, A. Pettorossi & M. Proietti (2001): Verifying CTL Properties of Infinite State Systems by Specializing Constraint Logic Programs. In: Proceedings of the ACM SIGPLAN Workshop on Verifica-tion and Computational Logic VCL’01, Florence (Italy), Technical Report DSSE-TR-2001-3, University of Southampton, UK, pp. 85-96. |
| [17] | M. Foley & C. A. R. Hoare (1971): Proof of a Recursive Program: Quicksort. Comput. J. 14(4), pp. 391-395, doi:10.1093/comjnl/14.4.391. · Zbl 0231.68011 · doi:10.1093/comjnl/14.4.391 |
| [18] | L. Fribourg & H. Olsén (1997): A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2(3/4), pp. 305-335, doi:10.1023/A:1009747629591. · Zbl 0889.68025 · doi:10.1023/A:1009747629591 |
| [19] | S. Grebenshchikov, N. P. Lopes, C. Popeea & A. Rybalchenko (2012): Synthesizing software verifiers from proof rules. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, pp. 405-416, doi:10.1145/2345156.2254112. · doi:10.1145/2345156.2254112 |
| [20] | J. Hamza, N. Voirol & V. Kuncak (2019): System FR: formalized foundations for the Stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA), pp. 166:1-166:30, doi:10.1145/3360592. · doi:10.1145/3360592 |
| [21] | C. A. R. Hoare (1961): Algorithm 64: Quicksort. Commun. ACM 4(7), p. 321, doi:10.1145/366622. 366644. · doi:10.1145/366622.366644 |
| [22] | C.A.R. Hoare (1969): An Axiomatic Basis for Computer Programming. CACM 12(10), pp. 576-580, 583, doi:10.1145/363235.363259. · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [23] | C. J. Hogger (1981): Derivation of Logic Programs. Journal of the ACM 28(2), pp. 372-392, doi:10.1145/ 322248.322258. · Zbl 0464.68021 · doi:10.1145/322248.322258 |
| [24] | H. Hojjat & Ph. Rümmer (2018): The ELDARICA Horn Solver. In N. Bjørner & A. Gurfinkel, editors: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 -November 2, 2018, IEEE, pp. 1-7, doi:10.23919/FMCAD.2018.8603013. · doi:10.23919/FMCAD.2018.8603013 |
| [25] | B. Kafle & J. P. Gallagher (2017): Constraint specialisation in Horn clause verification. Sci. Comput. Program. 137, pp. 125-140, doi:10.1016/j.scico.2017.01.002. · doi:10.1016/j.scico.2017.01.002 |
| [26] | A. Komuravelli, A. Gurfinkel, S. Chaki & E. M. Clarke (2013): Automatic Abstraction in SMT-Based Un-bounded Software Model Checking. In N. Sharygina & H. Veith, editors: Computer Aided Verification, Proceedings of the 25th International Conference CAV ’13, Saint Petersburg, Russia, July 13-19, 2013, Lec-ture Notes in Computer Science 8044, Springer, pp. 846-862, doi:10.1007/978-3-642-39799-8_59. · doi:10.1007/978-3-642-39799-8_59 |
| [27] | K. R. M. Leino (2013): Developing Verified Programs with Dafny. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE ’13, IEEE Press, pp. 1488-1490, doi:10.1109/ICSE.2013. 6606754. · doi:10.1109/ICSE.2013.6606754 |
| [28] | M. Leuschel & H. Lehmann (2000): Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction. In J. W. Lloyd, editor: Proceedings of the First International Conference on Computational Logic (CL 2000), London, UK, 24-28 July, Lecture Notes in Artificial Intelligence 1861, Springer-Verlag, pp. 101-115, doi:10.1007/3-540-44957-4_7. · Zbl 0983.68135 · doi:10.1007/3-540-44957-4_7 |
| [29] | E. Meijer, M. M. Fokkinga & R. Paterson (1991): Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. In J. Hughes, editor: Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings, Lecture Notes in Computer Science 523, Springer, pp. 124-144, doi:10.1007/3540543961_7. · doi:10.1007/3540543961_7 |
| [30] | M. Méndez-Lojo, J. A. Navas & M. V. Hermenegildo (2008): A Flexible, (C)LP-Based Approach to the Anal-ysis of Object-Oriented Programs. In: 17th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR ’07, Kongens Lyngby, Denmark, August 23-24, 2007, Lecture Notes in Computer Science 4915, Springer, pp. 154-168, doi:10.1007/978-3-540-78769-3_11. · Zbl 1179.68030 · doi:10.1007/978-3-540-78769-3_11 |
| [31] | D. Mordvinov & G. Fedyukovich (2017): Synchronizing Constrained Horn Clauses. In T. Eiter & D. Sands, editors: LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Rea-soning, Maun, Botswana, May 7-12, 2017, EPiC Series in Computing 46, EasyChair, pp. 338-355. Available at http://www.easychair.org/publications/paper/340359. · Zbl 1403.68243 |
| [32] | L. M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’08, Lecture Notes in Computer Science 4963, Springer, pp. 337-340, doi:10.1007/978-3-540-78800-3_24. · doi:10.1007/978-3-540-78800-3_24 |
| [33] | M. Odersky, L. Spoon & B. Venners (2011): Programming in Scala: A Comprehensive Step-by-Step Guide, 2nd edition. Artima Incorporation, Sunnyvale, CA, USA. |
| [34] | J. C. Peralta, J. P. Gallagher & H. Saglam (1998): Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In G. Levi, editor: Proceedings of the 5th International Symposium on Static Analysis, SAS ’98, Lecture Notes in Computer Science 1503, Springer, pp. 246-261, doi:10.1007/ 3-540-49727-7_15. · doi:10.1007/3-540-49727-7_15 |
| [35] | A. Pettorossi & M. Proietti (1989): Decidability Results and Characterization of Strategies for the Develop-ment of Logic Programs. In G. Levi & M. Martelli, editors: Proceedings of the Sixth International Conference on Logic Programming, Lisbon, Portugal, The MIT Press, pp. 539-553. |
| [36] | Tuan-Hung Pham, Andrew Gacek & Michael W. Whalen (2016): Reasoning About Algebraic Data Types with Abstractions. J. Autom. Reason. 57(4), pp. 281-318, doi:10.1007/s10817-016-9368-2. · Zbl 1386.68104 · doi:10.1007/s10817-016-9368-2 |
| [37] | A. Podelski & A. Rybalchenko (2007): ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In M. Hanus, editor: Practical Aspects of Declarative Languages, PADL ’07, Lecture Notes in Computer Science 4354, Springer, pp. 245-259, doi:10.1007/978-3-540-69611-7_16. · doi:10.1007/978-3-540-69611-7_16 |
| [38] | M. Proietti & A. Pettorossi (1995): Unfolding-Definition-Folding, in this Order, for Avoiding Unneces-sary Variables in Logic Programs. Theoretical Computer Science 142(1), pp. 89-124, doi:10.1016/ 0304-3975(94)00227-A. · Zbl 0873.68023 · doi:10.1016/0304-3975(94)00227-A |
| [39] | Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift & D. S. Warren (1997): Efficient Model Checking Using Tabled Resolution. In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV ’97), Lecture Notes in Computer Science 1254, Springer-Verlag, pp. 143-154, doi:10.1007/3-540-63166-6_16. · doi:10.1007/3-540-63166-6_16 |
| [40] | S. Renault, A. Pettorossi & M. Proietti (1998): Design, Implementation, and Use of the MAP Transformation System. R 491, IASI-CNR, Rome, Italy. Available at http://www.iasi.cnr.it/ proietti/system. html. |
| [41] | A. Reynolds & V. Kuncak (2015): Induction for SMT Solvers. In Deepak D’Souza, Akash Lal & Kim Guld-strand Larsen, editors: Verification, Model Checking, and Abstract Interpretation, Proceedings of the 16th International Conference VMCAI 2015, Mumbai, India, January 12-14, 2015, Lecture Notes in Computer Science 8931, Springer, pp. 80-98, doi:10.1007/978-3-662-46081-8_5. · Zbl 1432.68418 · doi:10.1007/978-3-662-46081-8_5 |
| [42] | Ph. Suter, M. Dotta & V. Kuncak (2010): Decision procedures for algebraic data types with abstractions. In M. V. Hermenegildo & J. Palsberg, editors: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, ACM, pp. 199-210, doi:10.1145/1706299.1706325. · Zbl 1312.68147 · doi:10.1145/1706299.1706325 |
| [43] | H. Tamaki & T. Sato (1984): Unfold/Fold Transformation of Logic Programs. In S.-Å. Tärnlund, editor: Proceedings of the Second International Conference on Logic Programming, ICLP ’84, Uppsala University, Uppsala, Sweden, pp. 127-138. |
| [44] | H. Unno, S. Torii & H. Sakamoto (2017): Automating Induction for Solving Horn Clauses. In Rupak Ma-jumdar & Viktor Kuncak, editors: Computer Aided Verification, Proceedings of the 29th International Con-ference CAV ’17, Heidelberg, Germany, Part II, Lecture Notes in Computer Science 10427, Springer, pp. 571-591, doi:10.1007/978-3-319-63390-9_30. · Zbl 1494.68064 · doi:10.1007/978-3-319-63390-9_30 |
| [45] | P. L. Wadler (1990): Deforestation: Transforming Programs to Eliminate Trees. Theoretical Computer Science 73, pp. 231-248, doi:10.1016/0304-3975(90)90147-A. · Zbl 0701.68013 · doi:10.1016/0304-3975(90)90147-A |
| [46] | F5. false :-A=false, qss(A). |
| [47] | a(A,B,C,D,E,F,G,H,I) :-A=J, B=0, C=0, D=0, E=true, F=true, G=K, H=L, I=M, N=0, O=0, P=0, Q=J, R=true, S=J, T=true, J>=0, new2(J,T,Q,S,R,P,K,O,L,N,M). |
| [48] | new2(A,B,C,D,E,F,G,H,I,J,K) :-A=L, B=true, C=L, D=L, E=true, F=0, G=true, H=0, J=0, K=M, L>=0, new3(L,M,D,E,H,I). |
| [49] | new2(A,B,C,D,E,F,G,H,I,J,K) :-A=L, B=true, C=L, D=L, E=true, F=0, G=M, H=0, J=0, K=N, O=true, P=Q, Q-L=< -1, Q>=0, new6(C,L,O,P,M,Q,N,D,E,H,I). |
| [50] | new3(A,B,C,D,E,F) :-A=C, B=true, D=true, E=0, F=true, C>=0. |
| [51] | new3(A,B,C,D,E,F) :-A=G, B=H, C=G, D=true, E=0, F=H, I=true, G>=0, J-G>=0, new10(G,I,J,H). |
| [52] | new6(A,B,C,D,E,F,G,H,I,J,K) :-A=L, B=L, C=true, D=F, E=true, G=M, H=L, I=true, J=0, F>=0, L-F>=0, new7(L,M,H,I,J,K). |
| [53] | new6(A,B,C,D,E,F,G,H,I,J,K) :-A=L, B=L, C=true, D=F, E=false, G=false, H=L, I=true, J=0, M=true, F>=1, L-F>=0, new9(A,L,M,H,I,J,K). |
| [54] | new6(A,B,C,D,E,F,G,H,I,J,K) :-A=L, B=L, C=true, D=F, E=M, G=N, H=L, I=true, J=0, O=true, P=Q, Q-L=< -1, F>=0, Q-F>=0, new6(A,L,O,P,M,Q,N,H,I,J,K). |
| [55] | new7(A,B,C,D,E,F) :-A=C, B=true, D=true, E=0, F=true, C>=0. 20. new7(A,B,C,D,E,F) :-A=G, B=H, C=G, D=true, E=0, F=H, I=true, G>=0, J-G>=0, new10(G,I,J,H). |
| [56] | new9(A,B,C,D,E,F,G) :-A=D, B=D, C=true, E=true, F=0, G=true, D>=1. 22. new9(A,B,C,D,E,F,G) :-A=H, B=H, C=true, D=H, E=true, F=0, G=I, J=true, H>=1, K>=H, new10(H,J,K,I). |
| [57] | new9(A,B,C,D,E,F,G) :-A=H, B=H, C=true, D=H, E=true, F=0, I=true, H>=1, new9(A,H,I,D,E,F,G). |
| [58] | new10(A,B,C,D) :-B=true, D=true, A>=0, C-A>=0. |
| [59] | new10(A,B,C,D) :-A=E, B=true, D=false, F=true, E-C=< -1, E>=0, new11(E,F). |
| [60] | new10(A,B,C,D) :-A=E, B=true, D=F, G=true, E-C=<0, E>=0, H>=C, new10(E,G,H,F). |
| [61] | new11(A,B) :-A=C, B=true, D=true, C>=0, new11(C,D). |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
