Volume 7: January - December 1997

Issue 2: 1997


Verification of meta-interpreters

  • Verification of meta-interpreters
  • D. Pedreschi and S. Ruggieri

    Dipartimento di Informatica, Universita di Pisa, Corso Italia 40, 56125 Pisa, Italy. E-mail: {pedre,ruggieri}@di.unipi.it


    A novel approach to the verification of meta-interpreters is introduced. We apply a general purpose verification method for logic programs, to the case study of the Vanilla and other logic meta-interpreters. We extend the standard notion of declarative correctness, and design a criterion for proving correctness of meta-interpreters in a general sense, including amalgamated and reflective meta-interpreters. The contribution of this paper can be summarized as follows: under certain natural assumptions, all interesting verification properties lift up from the object program to the meta-program, including partial correctness, termination, absence of errors, call patterns persistence, correct instances of queries, computed instances of queries. Interestingly, it is possible to establish these results on the basis of purely declarative reasoning, using the mentioned proof method. We believe that the obtained results illustrate the broad applicability of the adopted verification principles.

    Keywords: Meta-programming, logic programming, verification of logic programs, Vanilla

    Pages: 267 - 303

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Part of the OUP Journals World Wide Web service.

    Last modification: 22 Jul 1997

    Copyright© Oxford University Press, 1997.