Abstract
We present in this paper a methodology for verifying the partial correctness of programs written in a logic programming language with modules supporting local and contextual definitions of predicates. The methodology is a generalization of the one described in [5] and [6], originally developed for ordinary logic programs. To deal with the aspects of locality and contextual dependency, we introduce specifications for predicates in modules that are parametric on the context-dependent predicates. The verification of a program then consists in showing that for all possible contexts, what is true in those contexts satisfies the specification. The inductive technique introduced in [5, 6] is also generalized for the purpose of this verification. We then extend this technique to open programs consisting of isolated modules, and propose a compositional approach to the verification of modular programs.
Work partially supported by JNICT scholarship BD/5403/95, JNICT project PRAXIS XXI 2/2.1/MAT/46/94 (ESCOLA), and ESPRIT BRP 9102 (COORDINATION).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K.R. Apt. Program Verification and Prolog. In E. Borger, editor, Specification and Validation Methods for Programming Languages and Systems, Oxford University Press, 1994.
K.R. Apt and E. Marchiori. Reasoning about Prolog Programs: from Modes through Types to Assertions. To appear in Formal Aspects in Computing, 1994.
A. Brogi, E. Lamma, and P. Mello. A General Framework for Structuring Logic Programs. C.N.R. Technical Report “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo”, N. 4/1, May 1990.
K.L. Clark. Predicate Logic as a Computational Formalism. Research Monograph 79/59 TOC, Imperial College, London, December 1979.
P. Deransart. Proof Methods of Declarative Properties of Definite Programs. Theoretical Computer Science 118, pages 99–166, 1993.
P. Deransart and J. Małuszyński. A Grammatical View of Logic Programming. Cambridge, MA, 1993. The MIT Press.
L. Giordano and A. Martelli. A Modal Reconstruction of Blocks and Modules in Logic Programming. In V. Saraswat and K. Ueda, editors, Logic Programming: Proceedings of the 1991 International Symposium, 1991. The MIT Press.
L. Giordano, A. Martelli, and G. Rossi. Local Definitions with Static Scope Rules in Logic Programming. In International Conference on Fifth Generation Computer Systems 1988, pages 389–396, Tokyo, Japan, 1988. ICOT.
J.-M. Jacquet and L. Monteiro. Comparative Semantics for a Parallel Contextual Logic Programming Language. In Logic Programming: Proceedings of the 1990 North-American Conference, pages 195–214, 1990. The MIT Press.
A. Lallouet. Une Sémantique Inductive à la Herbrand pour la Programmation Logique Contextuelle. Application à une Notion de Correction Partielle. Journées Francophones de la Programmation Logique, Bordeaux, France, 1994.
A. Lallouet. Preuves Compositionelles en Programmation Logique. Journées Francophones de la Programmation Logique, Dijon, France, 1995.
F. McCabe. L&O: Logic and Objects. International Series in Computer Science. Prentice-Hall International, 1992.
P. Mello. Inheritance as Combination of Horn Clause Theories. In D. Nardi and M. Simi, editors, Inheritance Hierarchies in Knowledge Representation and Programming Languages, chapter 17, pages 275–289. Wiley, Chichester, UK, 1989.
D. Miller. A Theory of Modules for Logic Programming. In R.M. Keller, editor, 1986 Symposium on Logic Programming, pages 106–114, Washington, DC, 1986. IEEE Computer Society Press.
D. Miller. Lexical Scoping as Universal Quantification. In G. Levi and M. Martelli, editors, Logic Programming: Proceedings of the 6th International Conference, pages 268–283, 1989. The MIT Press.
D. Miller. A Logical Analysis of Modules in Logic Programming. Journal of Logic Programming, 6:79–108, 1989.
L. Monteiro. The Semantics of Contextual Logic Programming. Technical Report UNL DI-5/89, Dept. Informática, Universidade Nova de Lisboa, 1989.
L. Monteiro and A. Porto. Contextual Logic Programming. In G. Levi and M. Martelli, editors, Logic Programming: Proceedings of the 6th International Conference, pages 284–299, 1989. The MIT Press.
L. Monteiro and A. Porto. Semantic and Syntactic Inheritance in Logic Programming. In J. Darlington and R. Dietrich, editors, Declarative Programming, Sasbachwalden 1991, “Workshops in Computing” series, 1992. Springer-Verlag.
L. Monteiro and A. Porto. A Language for Contextual Logic Programing. In K.R. Apt, J.W. de Bakker, and J.J.M.M. Rutten, editors, Logic Programming Languages: Constraints, Functions, and Objects, pages 115–147, 1993. The MIT Press.
Y. Moscowitz and E. Shapiro. Lexical Logic Programs. In K. Furukawa, editor, Logic Programming: Proceedings of the 8th International Conference, pages 349–363, 1991. The MIT Press.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pedro, V., Monteiro, L. (1996). Modules and specifications. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds) Logics in Artificial Intelligence. JELIA 1996. Lecture Notes in Computer Science, vol 1126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61630-6_20
Download citation
DOI: https://doi.org/10.1007/3-540-61630-6_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61630-6
Online ISBN: 978-3-540-70643-4
eBook Packages: Springer Book Archive