Loop invariants: Analysis, classification, and examples

Abstract

Software verification has emerged as a key concern for ensuring the continued progress of information technology. Full verification generally requires, as a crucial step, equipping each loop with a “loop invariant.” Beyond their role in verification, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, finding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common flavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs.

We performed a systematic identification, validation, and classification of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study, governing how invariants are derived from postconditions; it proposes a taxonomy of invariants according to these patterns; and it presents its application to the algorithms reviewed. The discussion also shows the need for high-level specifications based on “domain theory.” It describes how the invariants and the corresponding algorithms have been mechanically verified using an automated program prover; the proof source files are available. The contributions also include suggestions for invariant inference and for model-based specification.

References

1. Samson Abramsky and Achim Jung. 1994. Domain theory. In Handbook of Logic in Computer Science III, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (Eds.). Oxford University Press.
2. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. 2007. Invariant synthesis for combined theories. In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’07), Byron Cook and Andreas Podelski (Eds.), Lecture Notes in Computer Science, vol. 4349. Springer, 378--394.
3. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A static analyzer for large safety-critical software. In Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’03). ACM, 196--207.
4. Joshua Bloch. 2006. Extra, Extra -- Read all about it: Nearly all binary searches and mergesorts are broken. http://googleresearch.blogspot.ch/2006/06/extra-extra-read-all-about-it -nearly.html. (2006).
5. Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konečný, and Tomáš Vojnar. 2009. Automatic verification of integer array programs. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09), Ahmed Bouajjani and Oded Maler (Eds.), Lecture Notes in Computer Science, vol. 5643. Springer, 157--172.
6. Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation. Springer.
7. Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s decidable about arrays? In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06), E. Allen Emerson and Kedar S. Namjoshi (Eds.), Lecture Notes in Computer Science, vol. 3855. Springer, 427--442.
8. Bruno Buchberger. 2006. Mathematical theory exploration. In Proceedings of the 3rd International Conference on Automated Reasoning (IJCAR'66). Lecture Notes in Computer Science, vol. 4130. Springer, 1--2.
9. Bor-Yuh Evan Chang and K. Rustan M. Leino. 2005. Abstract Interpretation with alien expressions and heap structures. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’05), Radhia Cousot (Ed.), Lecture Notes in Computer Science Series, vol. 3385. Springer, 147--163.
10. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press.
11. Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear invariant generation using non-linear constraint solving. In Proceedings of the 15th International Conference on Computer Aided Verification(CAV’03), Jr. Warren A. Hunt and Fabio Somenzi (Eds.), Lecture Notes in Computer Science, vol. 2725. Springer, 420--432.
12. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). MIT Press.
13. Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages (POPL’77). 238--252.
14. Patrick Cousot and Nicolas Halbwachs. 1978. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages (POPL’78). 84--96.
15. Christoph Csallner, Nikolai Tillman, and Yannis Smaragdakis. 2008. DySy: Dynamic symbolic execution for invariant inference. In Proceedings of the 30th International Conference on Software Engineering (ICSE’08), Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn (Eds.). ACM, 281--290.
16. Guido de Caso, Diego Garbervetsky, and Daniel Gorín. 2009. Reducing the number of annotations in a verification-oriented imperative language. In Proceedings of Automatic Program Verification.
17. Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall.
18. Eiffel. 2006. Standard ECMA-367. Eiffel: Analysis, design and programming language. (2006).
19. Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. 2001. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions of Software Engineering 27, 2 (2001), 99--123.
20. Robert W. Floyd. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science J. T. Schwartz (Ed.), Proceedings of Symposia in Applied Mathematics Series, vol. 19. American Mathematical Society, 19--32.
21. Gordon Fraser and Andreas Zeller. 2011. Exploiting common object usage in test case generation. In Proceedings of the IEEE 4th International Conference on Software Testing, Verification and Validation (ICST’11). IEEE Computer Society, 80--89.
22. Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi. 2012. Modeling Time in Computing. Monographs in Theoretical Computer Science. An CATCS Series. Springer.
23. Carlo A. Furia and Bertrand Meyer. 2010. Inferring loop invariants using postconditions. In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig (Eds.), Lecture Notes in Computer Science Series, vol. 6300. Springer, 277--300.
24. Michael R. Garey and David S. Johnson. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman.
25. Carlo Ghezzi, Andrea Mocci, and Mattia Monga. 2009. Synthesizing intensional behavior models by graph transformation. In Proceedings of the 31st International Conference on Software Engineering (ICSE’09). IEEE, 430--440.
26. David Gries. 1981. The Science of Programming. Springer-Verlag.
27. Neelam Gupta and Zachary V. Heidepriem. 2003. A new structural coverage criterion for dynamic detection of program invariants. In 18th IEEE International Conference on Automated Software Engineering (ASE’03). IEEE Computer Society, 49--59.
28. John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew J. Parkinson. 2012. Behavioral interface specification languages. ACM Comput. Surv. 44, 3 (2012), 16.
29. Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, and Andrei Voronkov. 2010. Invariant and type inference for matrices. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’10). Lecture Notes in Computer Science. Springer.
30. C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576--580.
31. C. A. R. Hoare. 1972. Proof of correctness of data representations. Acta Inf. 1 (1972), 271--281.
32. C. A. R. Hoare. 2003. The verifying compiler: A grand challenge for computing research. J. ACM 50, 1 (2003), 63--69.
33. Mikoláš Janota. 2007. Assertion-based loop invariant generation. In Proceedings of the 1st International Workshop on Invariant Generation (WING’07).
34. Ranjit Jhala and Rupak Majumdar. 2009. Software model checking. Comput. Surveys 41, 4 (2009).
35. Michael Karr. 1976. Affine relationships among variables of a program. Acta Informatica 6 (1976), 133--151.
36. Hans Kellerer, Ulrich Pferschy, and David Pisinger. 2004. Knapsack problems. Springer.
37. Donald E. Knuth. 2011. The Art of Computer Programming (1st ed., Volumes 1--4A). Addison-Wesley. 1968--1973.
38. Laura Kovács and Andrei Voronkov. 2009. Finding loop invariants for programs over arrays using a theorem prover. In Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering (FASE’09), Marsha Chechik and Martin Wirsing (Eds.), Lecture Notes in Computer Science Series, vol. 5503. Springer, 470--485.
39. Daniel Kroening and Ofer Strichman. 2008. Decision Procedures: An Algorithmic Point of View. Monographs in Theoretical Computer Sciences. An EATCS Series. Springer.
40. Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, and Thomas Wies. 2009. Intra-module Inference. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09), Ahmed Bouajjani and Oded Maler (Eds.), Lecture Notes in Computer Science Series, vol. 5643. Springer, 493--508.
41. Leslie Lamport. 1977. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3, 2 (1977), 125--143.
42. Leslie Lamport. 2009. Teaching concurrency. SIGACT News 40, 1 (2009), 58--62.
43. K. Rustan M. Leino. 2008. This is Boogie 2. (June 2008). (Manuscript KRML 178) http://research.microsoft.com/en-us/projects/boogie/.
44. Francesco Logozzo. 2004. Automatic inference of class invariants. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’04), Bernhard Steffen and Giorgio Levi (Eds.), Lecture Notes in Computer Science Series, vol. 2937. Springer, 211--222.
45. Kurt Mehlhorn and Peter Sanders. 2008. Algorithms and Data Structures: The Basic Toolbox. Springer.
46. Bertrand Meyer. 1980. A basis for the constructive approach to programming. In Proceedings of IFIP Congress 1980, Simon H. Lavington (Ed.). 293--298.
47. Bertrand Meyer. 1997. Object-oriented software construction (2nd ed.). Prentice Hall.
48. Carroll Morgan. 1994. Programming from Specifications (2nd ed.). Prentice Hall.
49. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2012. Using dynamic analysis to discover polynomial and array invariants. In Proceedings of the 34th International Conference on Software Engineering (ICSE’12). IEEE, 683--693.
50. Susan Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs. Acta Informatica 6 (1976), 319--340.
51. Christos H. Papadimitriou. 1993. Computational Complexity. Addison-Wesley.
52. Corina S. Păsăreanu and Willem Visser. 2004. Verification of Java programs using symbolic execution and invariant generation. In Proceedings of the 11th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science Series, vol. 2989. Springer, 164--181.
53. Jeff H. Perkings and Michael D. Ernst. 2004. Efficient incremental algorithms for dynamic detection of likely invariants. In Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT’04/FSE-12), Richard N. Taylor and Matthew B. Dwyer (Eds.). ACM, 23--32.
54. André Platzer. 2010. Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20, 1 (2010), 309--352.
55. Nadia Polikarpova, Ilinca Ciupa, and Bertrand Meyer. 2009. A comparative study of programmer-written and automatically inferred contracts. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’09). 93--104.
56. Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier.
57. Enric Rodríguez-Carbonell and Deepak Kapur. 2007. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42, 4 (2007), 443--476.
58. Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. 2004. Non-linear loop invariant generation using Gröbner bases. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’04), Neil D. Jones and Xavier Leroy (Eds.). ACM, 318--329.
59. Michael I. Shamos. 1978. Computational geometry. Ph.D.thesis Yale University. http://goo.gl/XiXNl.
60. J. Michael Spivey. 1992. Z Notation -- a reference manual (2nd ed.). Prentice Hall International Series in Computer Science. Prentice Hall.
61. Nikolai Tillmann, Feng Chen, and Wolfram Schulte. 2006. Discovering likely method specifications. In Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM’06). Lecture Notes in Computer Science Series, vol. 4260. 717--736.
62. Godfried T. Toussaint. 1983. Solving geometric problems with the rotating calipers. In Proceedings of IEEE MELECON.
63. Yi Wei, Carlo A. Furia, Nikolay Kazmin, and Bertrand Meyer. 2011a. Inferring Better Contracts. In Proceedings of the 33rd International Conference on Software Engineering (ICSE’11), Richard N. Taylor, Harald Gall, and Nenad Medvidović (Eds.). ACM, 191--200.
64. Yi Wei, Hannes Roth, Carlo A. Furia, Yu Pei, Alexander Horton, Michael Steindorfer, Martin Nordio, and Bertrand Meyer. 2011b. Stateful testing: Finding more errors in code and contracts. In Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE’11), Perry Alexander, Corina Pasareanu, and John Hosking (Eds.). ACM, 440--443.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification