Improving Execution Models of Logic Programs by Two-phase Abstract Interpretation

ETRI Journal ◽  
1995 ◽  
Vol 16 (4) ◽  
pp. 27-47
Author(s):  
Byeong-Mo Chang Chang ◽  
Kwang-Moo Choe Choe ◽  
Roberto Giacobazzi Giacobazzi
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs ◽  
Two Phase ◽  
Execution Models

scholarly journals Bottom-up abstract interpretation of logic programs

1994 ◽  
Vol 124 (1) ◽  
pp. 93-125 ◽  
Author(s):  
Michael Codish ◽  
Dennis Dams ◽  
Eyal Yardeni
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs ◽  
Bottom Up

scholarly journals A backward analysis for constraint logic programs

2002 ◽  
Vol 2 (4-5) ◽  
pp. 517-547 ◽  
Author(s):  
ANDY KING ◽  
LUNJIN LU
Keyword(s):  
Ad Hoc ◽  
Abstract Interpretation ◽  
Logic Program ◽  
Control Flow ◽  
Third Party ◽  
Logic Programs ◽  
Abstract Domains ◽  
Constraint Logic Programs ◽  
Backward Analysis ◽  
Computational Properties

One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If the logic program does not come with any documentation, then the programmer is forced to either experiment with queries in an ad hoc fashion or trace the control-flow of the program (backward) to infer the modes in which a predicate must be called so as to avoid an instantiation error. This paper presents an abstract interpretation scheme that automates the latter technique. The analysis presented in this paper can infer moding properties which if satisfied by the initial query, come with the guarantee that the program and query can never generate any moding or instantiation errors. Other applications of the analysis are discussed. The paper explains how abstract domains with certain computational properties (they condense) can be used to trace control-flow backward (right-to-left) to infer useful properties of initial queries. A correctness argument is presented and an implementation is reported.

scholarly journals Abstract interpretation and application to logic programs

1992 ◽  
Vol 13 (2-3) ◽  
pp. 103-179 ◽  
Author(s):  
Patrick Cousot ◽  
Radhia Cousot
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs

scholarly journals Optimality in goal-dependent analysis of Sharing

2009 ◽  
Vol 9 (05) ◽  
pp. 617-689 ◽  
Author(s):  
GIANLUCA AMATO ◽  
FRANCESCA SCOZZARI
Keyword(s):  
Logic Programming ◽  
Static Analysis ◽  
Abstract Interpretation ◽  
Logic Programs ◽  
Semantic Operators

AbstractWe face the problems of correctness, optimality, and precision for the static analysis of logic programs, using the theory of abstract interpretation. We propose a framework with a denotational, goal-dependent semantics equipped with two unification operators for forward unification (calling a procedure) and backward unification (returning from a procedure). The latter is implemented through a matching operation. Our proposal clarifies and unifies many different frameworks and ideas on static analysis of logic programming in a single, formal setting. On the abstract side, we focus on the domainsharingby Jacobs and Langen (The Journal of Logic Programming, 1992, vol. 13, nos. 2–3, pp. 291–314) and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, and forward and backward unifications. We show that the abstract unification operators are strictly more precise than those in the literature defined over the same abstract domain. In some cases, our operators are more precise than those developed for more complex domains involving linearity and freeness.

An abstract interpretation scheme for identifying inherent parallelism in logic programs

1990 ◽  
Vol 7 (2-3) ◽  
pp. 273-324 ◽  
Author(s):  
Arvind K. Bansal ◽  
Leon S. Sterling
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs

RECOGNIZING NON-FLOUNDERING LOGIC PROGRAMS AND GOALS

1990 ◽  
Vol 01 (02) ◽  
pp. 151-163 ◽  
Author(s):  
ROBERTO BARBUTI ◽  
MAURIZIO MARTELLI
Keyword(s):  
Logic Programming ◽  
Abstract Interpretation ◽  
Logic Programs ◽  
Negation As Failure ◽  
Proof Procedure ◽  
Resolution Proof

The introduction of negation in Logic Programming using the Negation as Failure Rule causes some problems regarding the completeness of the SLDNF-Resolution proof procedure. One of the causes of incompleteness arises when evaluating a non-ground negative literal. This is solved by forbidding these evaluations. Obviously, there is the possibility of having only non-ground negative literals in the goal (the floundering of the goal). There is a class of programs and goals (allowed) that has been proved to have the non-floundering property. In this paper an algorithm is proposed which recognizes a wider class of programs with this property and which is based on abstract interpretation techniques.

Sign in / Sign up

Export Citation Format

Share Document