Abstract
In this paper we discuss the similarities between program specialisation and inductive theorem proving, and then show how program specialisation can be used to perform inductive theorem proving. We then study this relationship in more detail for a particular class of problems (verifying infinite state Petri nets) in order to establish a clear link between program specialisation and inductive theorem proving. In particular, we use the program specialiser ecce to generate specifications, hypotheses and proof scripts in the theory format of the proof assistant Isabelle. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of ecce’s verification process and of the correspondence between program specialisation and inductive theorem proving.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artificial Intelligence 62, 185–253 (1993)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)
De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.H.: Conjunctive partial deduction: Foundations, control, algorithms and experiments. The Journal of Logic Programming 41(2 & 3), 231–277 (1999)
Finkel, A.: The minimal coverability graph for Petri nets. In: Rozenberg, G. (ed.) APN 1993. LNCS, vol. 674, pp. 210–243. Springer, Heidelberg (1993)
Gallagher, J.P., Peralta, J.C.: Regular tree languages as an abstract domain in program specialisation. Higher Order and Symbolic Computation 14(2–3), 143–172 (2001)
Glück, R., Jørgensen, J.: Generating transformers for deforestation and supercompilation. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 432–448. Springer, Heidelberg (1994)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)
Lehmann, H., Leuschel, M.: Generating inductive verification proofs for Isabelle using the partial evaluator Ecce. Technical Report DSSE-TR-2002-02, Department of Electronics and Computer Science, University of Southampton, UK (September 2002)
Leuschel, M.: The ecce partial deduction system and the dppd library of benchmarks (1996-2002), Obtainable via http://www.ecs.soton.ac.uk/~mal
Leuschel, M.: A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems (May 2004) (to appear)
Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2(4 & 5), 461–515 (2002)
Leuschel, M., Jørgensen, J., Vanhoof, W., Bruynooghe, M.: Offline specialisation in Prolog using a hand-written compiler generator. Theory and Practice of Logic Programming 4(1), 139–191 (2004)
Leuschel, M., Lehmann, H.: Solving coverability problems of Petri nets by partial deduction. In: Gabbrielli, M., Pfenning, F. (eds.) Proceedings of PPDP 2000, Montreal, Canada, pp. 268–279. ACM Press, New York (2000)
Leuschel, M., Martens, B., De Schreye, D.: Controlling generalisation and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems 20(1), 208–258 (1998)
Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)
Lloyd, J.W., Shepherdson, J.C.: Partial evaluation in logic programming. The Journal of Logic Programming 11(3&4), 217–242 (1991)
Marriott, K., Naish, L., Lassez, J.-L.: Most specific logic programs. Annals of Mathematics and Artificial Intelligence 1, 303–338 (1990)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Pettorossi, A., Proietti, M.: Synthesis and transformation of logic programs using unfold/fold proofs. The Journal of Logic Programming 41(2&3), 197–230 (1999)
Puebla, G., Hermenegildo, M.: Abstract specialization and its applications. In: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2003), June 2003, pp. 29–43. ACM Press, New York (2003)
Turchin, V.F.: Program transformation with metasystem transitions. Journal of Functional Programming 3(3), 283–313 (1993)
Turchin, V.F.: Metacomputation: Metasystem transitions plus supercompilation. In: Danvy, O., Glück, R., Thiemann, P. (eds.) Dagstuhl Seminar 1996. LNCS, vol. 1110, pp. 482–509. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lehmann, H., Leuschel, M. (2004). Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. In: Bruynooghe, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2003. Lecture Notes in Computer Science, vol 3018. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25938-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-25938-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22174-6
Online ISBN: 978-3-540-25938-1
eBook Packages: Springer Book Archive