Proving Theorems by Program Transformation

• Autorzy: Fioravanti F. , Pettorossi A. , Proietti M. , Senni V.
• Języki publikacji: EN

Abstrakty

EN

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.

Słowa kluczowe

EN

automated theorem proving; constraint logic programming; program specialization; program transformation; quantifier elimination; temporal logics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 127, nr 1-4
• Strony: 115--134
• Opis fizyczny: Bibliogr. 38 poz.

Twórcy

autor

Fioravanti F.

• University of Chieti-Pescara, Pescara, Italy

autor

Pettorossi A.

• University of Rome Tor Vergata, Via del Politecnico 1, 00133 Rome, Italy

autor

Proietti M.

• IASI-CNR, Viale Manzoni 30, 00185 Rome, Italy

autor

Senni V.

• IMT, Institute for Advanced Studies, Lucca, Italy

Bibliografia

• [1] The MAP transformation system. http: //www. iasi. cnr. it/^proietti/system. html. Also available via WEB interface: http://www.map.uniroma2.it/mapweb.
• [2] G. R. Andrews. Concurrent Programming: Principles and Practice. Addison-Wesley, 1991.
• [3] K. R. Apt and R. N. Bol. Logic programming and negation: A survey. Journal of Logic Programming, 19, 20:9-71, 1994.
• [4] R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44-67, January 1977.
• [5] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [6] B. Courcelle. Equivalences and transformations of regular systems - Applications to recursive program schemes and grammars. Theoretical Computer Science, 42:1-122, 1986.
• [7] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th ACM Symposium on Principles of Programming Languages, POPL ’78, 84-96. ACM Press, 1978.
• [8] E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying Programs via Iterated Specialization. In Proc. ACMSIGPLAN Workshop PEPM’13. 43-52, ACM, New York, USA, 2013.
• [9] S. Etalle andM. Gabbrielli. Transformations of CLP modules. Theoretical Comp. Sci., 166:101-146, 1996.
• [10] F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying CTL properties of infinite state systems by specializing constraint logic programs. In Proc. ACM SIGPLAN Workshop VCL’01, Technical Report DSSE-TR-2001-3, 85-96. University of Southampton, UK, 2001.
• [11] F. Fioravanti, A. Pettorossi, and M. Proietti. Combining logic programs and monadic second order logics by program transformation. In M. Leuschel, ed., Proc. LOPSTR ’02, Lecture Notes in Computer Science 2664, 160-181. Springer, 2003.
• [12] F. Fioravanti, A. Pettorossi, and M. Proietti. Transformation rules for locally stratified constraint logic programs. In K.-K. Lau and M. Bruynooghe, eds., Program Development in Computational Logic, Lecture Notes in Computer Science 3049, 292-340. Springer, 2004.
• [13] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming. Special Issue 25th GULP, 13(2): 175-199, 2013.
• [14] M. C. Hennessy. An Introduction to a Calculus of Communicating Systems. SRC Grant GR/A/75125, University of Edinburgh, Scotland, 1982.
• [15] J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19/20:503581, 1994.
• [16] R. Jhala andR. Majumdar. Software model checking. ACM Computing Surveys, 41(4):21:1-21:54, 2009.
• [17] L. Kott. Unfold/fold program transformation. In M. Nivat and J.C. Reynolds, eds., Algebraic Methods in Semantics, Cambridge University Press, 411-434, 1985.
• [18] M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In A. Bossi, ed., Proc. LOPSTR ’99, LNCS 1817. Springer, 63-82, 2000.
• [19] J. W. Lloyd. Foundations of Logic Programming. Second Edition, Springer, Berlin, 1987.
• [20] R. Loos and V Weispfenning. Applying linear quantifier elimination. The Comp. Jour., 36(5):450-462, 1993.
• [21] J. McCarthy. Towards a mathematical science of computation. In C. M. Popplewell, ed., Information Processing, Proc. IFIP’62,21-28, Amsterdam, North Holland, 1963.
• [22] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
• [23] J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In M. Leuschel, ed., Proc. LOPSTR ’02, Lecture Notes in Computer Science 2664, Springer, 90-108, 2003.
• [24] J. C. Peralta, J. P. Gallagher, and H. Saglam. Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In G. Levi, ed., Proc. SAS’98, LNCS 1503, 246-261. Springer, 1998.
• [25] A. Pettorossi and M. Proietti. Transformation of logic programs: Foundations and techniques. Journal of Logic Programming, 19, 20:261-320, 1994.
• [26] A. Pettorossi and M. Proietti. Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming, 41(2&3):197-230, 1999.
• [27] A. Pettorossi and M. Proietti. Perfect model checking via unfold/fold transformations. In J. W. Lloyd, ed., Proc. CL 2000, Lecture Notes in Artificial Intelligence 1861, 613-628. Springer, 2000.
• [28] A. Pettorossi, M. Proietti, and V Senni. Proving properties of constraint logic programs by eliminating existential variables. In S. Etalle and M. Truszczynski, eds., Proc. ICLP ’06, Lecture Notes in Computer Science 4079, 179-195. Springer, 2006.
• [29] A. Pettorossi, M. Proietti, and V Senni. Transformations of logic programs on infinite lists. Theory and Practice of Logic Programming, Special Issue ICLP’10, Edinburgh, Scotland, 10(4-6): 383-399, 2010.
• [30] A. Pettorossi, M. Proietti, and V. Senni. Constraint-based correctness proofs for logic program transformations. Formal Aspects of Computing, 24:569-594, 2012.
• [31] M. Proietti and A. Pettorossi. Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science, 142(1):89-124, 1995.
• [32] M. O. Rabin. Decidable theories. In J. Barwise, ed., Handbook of Mathematical Logic, 595-629. North- Holland, 1977.
• [33] A. Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, and S. A. Smolka. Verification of parameterized systems using logic program transformations. In Proc. TACAS 2000, Lecture Notes in Computer Science 1785, 172-187. Springer, 2000.
• [34] H. Seki. Unfold/fold transformation of stratified programs. Theoretical Computer Science, 86:107-139,1991.
• [35] H. Seki. On inductive and coinductive proofs via unfold/fold transformations. In D. De Schreye, ed., Proc. LOPSTR ’09, Lecture Notes in Computer Science 6037, 82-96. Springer, 2010.
• [36] H. Seki. Proving properties of co-logic programs with negation by program transformations. In E. Albert, ed., Proc. LOPSTR ’12, Lecture Notes in Computer Science 7844, 213-227. Springer, 2013.
• [37] L. Simon, A. Mallya, A. Bansal, and G. Gupta. Coinductive logic programming. In S. Etalle and M. Truszczynski, eds., Proc. ICLP’06, Lecture Notes in Computer Science 4079, 330-345. Springer, 2006.
• [38] H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In S.-A. Tarnlund, ed., Proc. ICLP ’84, Uppsala University, Uppsala, Sweden, 127-138,1984.