Relational analysis of algebraic datatypes

ABSTRACT

We present a technique that enables the use of finite model finding to check the satisfiability of certain formulas whose intended models are infinite. Such formulas arise when using the language of sets and relations to reason about structured values such as algebraic datatypes. The key idea of our technique is to identify a natural syntactic class of formulas in relational logic for which reasoning about infinite structures can be reduced to reasoning about finite structures. As a result, when a formula belongs to this class, we can use existing finite model finding tools to check whether the formula holds in the desired infinite model.

REFERENCES

• 1: The Alloy project. http://alloy.mit.edu/.
• 2: Egidio Astesiano , Michel Bidoit , Hélène Kirchner , Bernd Krieg-Brückner , Peter D. Mosses , Donald Sannella , Andrzej Tarlecki, CASL: the common algebraic specification language, Theoretical Computer Science, v.286 n.2, p.153-196, 17 September 2002 [doi>10.1016/S0304-3975(01)00368-1]
• 3: Richard Bird, Introduction to Functional Programming, Pearson Education, 1998
• 4: Adel Bouhoula , Jean-Pierre Jouannaud , José Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, v.236 n.1-2, p.35-132, April 6, 2000 [doi>10.1016/S0304-3975(99)00206-6]
• 5: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 6: Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri, NUSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, p.495-499, July 06-10, 1999
• 7: K. Claessen and N. Sörensson. New techniques that improve MACE-style model finding. In Model Computation, 2003.
• 8: K. J. Compton and C. W. Henson. A uniform method for proving lower bounds on the computational complexity of logical theories. Annals of Pure and Applied Logic, 48(1):1--79, July 1990.
• 9: J. Ferrante and C. W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979.
• 10: M. Gogolla, J. Bohling, and M. Richters. Validating UML and OCL models in USE by automatic snapshot generation. Journal on Software and System Modeling, 2005. to appear.
• 11: John V. Guttag, Abstract data types, then and now, Software pioneers: contributions to software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
• 12: John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
• 13: Volker Haarslev , Ralf Möller, RACER System Description, Proceedings of the First International Joint Conference on Automated Reasoning, p.701-706, June 18-23, 2001
• 14: W. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.
• 15: I. Horrocks. Using an expressive description logic: FaCT or fiction? In International Conference on Principles of Knowledge Representation and Reasoning, pages 636--647, 1998.
• 16: N. Immerman, A. M. Rabinovich, T. W. Reps, S. Sagiv, and G. Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In Computer Science Logic (CSL), pages 160--174, 2004.
• 17: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 18: Daniel Jackson, Object models as heap invariants, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
• 19: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 20: J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1--33, Washington, D.C., 1990. IEEE Computer Society Press.
• 21: Nils Klarlund , Anders Møller , Michael I. Schwartzbach, MONA Implementation Secrets, Revised Papers from the 5th International Conference on Implementation and Application of Automata, p.182-194, July 24-25, 2000
• 22: V. Kuncak and D. Jackson. On relational analysis of algebraic datatypes. Technical Report 985, MIT, April 2005.
• 23: V. Kuncak and M. Rinard. On the theory of structural subtyping. Technical Report 879, Laboratory for Computer Science, Massachusetts Institute of Technology, 2003.
• 24: Viktor Kuncak , Martin Rinard, Structural Subtyping of Non-Recursive Types is Decidable, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.96, June 22-25, 2003
• 25: X. Leroy. The Objective Caml system, release 3.08, July 2004.
• 26: M. Leuschel and M. J. Butler. ProB: A model checker for B. In Formal Methods Europe, pages 855--874, 2003.
• 27: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 28: M. J. Maher. Complete axiomatizations of the algebras of the finite, rational, and infinite trees. IEEE Symposium on Logic in Computer Science, 1988.
• 29: A. I. Malćev. The Metamathematics of Algebraic Systems, volume 66 of Studies in Logic and The Foundations of Mathematics. North Holland, 1971.
• 30: Darko Marinov , Martin C. Rinard, Automatic testing of software with structurally complex inputs, Massachusetts Institute of Technology, Cambridge, MA, 2005
• 31: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 32: W. McCune. MACE 2.0 Reference Manual and Guide. ArXiv Computer Science e-prints, June 2001.
• 33: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 34: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 35: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 36: Derek C. Oppen, Reasoning About Recursively Defined Data Structures, Journal of the ACM (JACM), v.27 n.3, p.403-411, July 1980 [doi>10.1145/322203.322204]
• 37: M. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1--35, 1969.
• 38: James Rumbaugh , Ivar Jacobson , Grady Booch, The Unified Modeling Language reference manual, Addison-Wesley Longman Ltd., Essex, UK, 1998
• 39: James Rumbaugh , Michael Blaha , William Premerlani , Frederick Eddy , William Lorensen, Object-oriented modeling and design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 40: T. Sturm and V. Weispfenning. Quantifier elimination in term algebras: The case of finite languages. In V. G. Ganzha, E. W. Mayr, and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (CASC), TUM Muenchen, 2002.
• 41: Ralf Treinen, Feature trees over arbitrary structures, Specifying syntactic structures, Center for the Study of Language and Information, Stanford, CA, 1997
• 42: K. N. Venkataraman, Decidability of the purely existential fragment of the theory of term algebras, Journal of the ACM (JACM), v.34 n.2, p.492-510, April 1987 [doi>10.1145/23005.24037]
• 43: T. Zhang, H. B. Sipma, and Z. Manna. Decision procedures for recursive data structures with integer constraints. In International Joint Conference on Automated Reasoning, volume 3097 of LNCS, pages 157--167, 2004.
• 44: T. Zhang, H. B. Sipma, and Z. Manna. Term algebras with length function and bounded quantifier alternation. In Theorem Proving in Higher-Order Logics, volume 3223 of LNCS, pages 321--336, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs; Mechanical verification; Specification techniques

General Terms:
Design, Reliability, Theory, Verification

Keywords:
algebraic datatypes, constraint solving, model checking, model finding, transitive closure logic