Abstract
This paper presents a study of correctness of pure Prolog programs, based on the technique of Abstract Interpretation for logic programs. The notion of (partial) correctness of a program relies on the type pre-analysis of call and success substitutions compared (dynamically) with concrete data-flow. It is possible to deduce, by the mean of a global static analysis, properties on variables of the analyzed program (groundness, type, sharing...) but also general properties of the entire program such as: how look the solutions like, the number of these solutions,.... The technique we propose is based on a novel approach of type inference (see [18, 7]) which relies on a recent method of global analysis for logic programs formalized within the abstract interpretation framework (see [18]).
This work was partially supported by the GRECO de programmation (METHEOL project)
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.
References
M. Bruynooghe A practical framework for the abstract interpretation of logic programs; 5ik ICLP—SLP 88;tutorial N°2.
P. De Boeck, B. Le Charlier Static analysis of prolog procedures for ensuring correctness; Proc. 2’ workshop on Programming Language Implementation and Logic Programming, Linköping university, Sweden, Aug 1990.
P. Cousot, R. Cousot Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixpoints;POPL 1977;Sigact Sigplan;pp 238–252.
M. Codish, D. Dams, E. Yardeni Bottom-up abstract interpretation of logic programs; technical report CS90–24 Weizmann institute.
M. Codish, D. Dams, E. Yardeni Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis; draft oct. 90 Weizmann Institute.
M-M. Corsini, G. Filè A complete framework for the abstract interpretation of logic programs: theory and application; research report Università di Padova.
M-M Corsini, K. Musumbu Type inference in Prolog: a new approach; to appear in proc. of Informatika9l.
S. Debray Static Inference of Modes and Data Dependencies in Logic Programs; Rep.87–15, Univ. of Arizona 1987.
S. Debray, D. Warren Automatic Mode Inference for Logic Programs; J. Logic Programming 1988 vol. 5;pp 207–229.
G. Filé, A. Cortesi Abstract interpretation of logic programs: an abstract domain for groundness, sharing, freeness and compoundness analysis; ACM Sigplan symposium on partial evaluation 91.
G. Janssens, M. Bruynooghe Deriving descriptions of possible values of program variables by means of abstract interpretation; draft revised version for Journal of Logic programming.
T. Kanamori, T. Kawamura Abstract interpretation based on OLDT resolution; ICOT research report 1990.
B. Le Charlier, K. Musumbu, P. Van Hentenryck A general abstract interpretation algorithm and its complexity analysis; ICLP 91; pp 64–78.
J. Lloyd Foundations of logic programming;Springer Verlag;series in symbolic of computation 1987.
C. Mellish Abstract Interpretation of Prolog programs; ICLP 86;LNCS 225;pp 463–474.
R. Milner A theory of type polymorphism in programming; Edinburgh internal report CSR 9–77.
A. Marién, G. Janssens, A. Mulkers, M. Bruynooghe The impact of abstract interpretation on code generation: an experiment in efficiency, ICLP 89;pp 33–47.
K. Musumbu Abstract interpretation of prolog programs;PHD thesis (in french); sept. 90.
K. Marriott, H. Sondergaard Bottom up abstract interpretation of logic programs; ICLP/SLP 88.
K. Marriott, H. Sondergaard Abstract interpretation of logic programs: the denotaional approach; GULP90.
T. Sato, H. Tamaki OLD resolution with tabulation ICLP 86;LNCS 225;pp 84–98.
E. Yardeni, E. Shapiro A type system for logic programs; Research report CS87–05 Weizmann Institute.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 Springer-Verlag London
About this paper
Cite this paper
Corsini, MM., Musumbu, K. (1992). Failure Analysis based on Abstract Interpretation. In: Darlington, J., Dietrich, R. (eds) Declarative Programming, Sasbachwalden 1991. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3794-8_19
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3794-8_19
Publisher Name: Springer, London
Print ISBN: 978-3-540-19735-5
Online ISBN: 978-1-4471-3794-8
eBook Packages: Springer Book Archive