33.tex






\subsection{Approximating program semantics}
\label{section.approx}

In this work we are mainly interested in checking program correctness.
However the representation of the verification condition (Proposition
\ref{ver.cond})
 as constraints (Lemma \ref{implication.as.constraints.lemma})
 can be used to obtain an approximation
of the semantics of a given program $P$. 
In the previous section we showed how a single implication from
Proposition \ref{ver.cond}
can be expressed by a constraint system $F_j(C)$.
We begin with constructing a constraint system representing all the
implications from the proposition.

Let us consider the constraints $F_j(C)$  ($j=1,\ldots,n_C$)
for each clause $C$ of $P$ with  $n_C$ body atoms.
Let  $F'_j(C)$ be  $F_j(C)$ with the variables renamed in
such a way that the only common variables of (distinct)
$F'_{j_1}(C_1)$, $F'_{j_2}(C_2)$ are $Call$ and  $Success$.
Let grammar $G_0$ specify the initial goals and the
constraint predicates.  So   \sem[G_0]{\Ca}\ is the set
of initial goals and of the allowed calls of constraints.
$\sem[G_0]{\Su}$
is (a superset of) the set of possible successes of constraint predicates.%
\footnote{
This approach can also be used when $P$ is a fragment of a program,
i.e.\ the clauses defining some predicates are missing in $P$.
Then the semantics of such predicates has to be specified by $G_0$.
The algorithm treats them as the constraint predicates.
Examples of such program fragments are programs using built-in predicates,
unfinished programs or modules of some bigger programs.
}
Thus $(\sem[G_0]\Ca, \sem[G_0]\Su)$ respects constraints.

Now any model $I$ of the constraint system
\[
{\cal C}(P) = \bigcup_{C\in P} \bigcup_j  F'_j(C) \ \cup\ G_0
\]
gives a specification
 $Spec=(I(\Ca),I(\Su))$
with respect to which $P$ is correct,
provided that $Spec$ respects constraints.
This follows immediately from Lemma \ref{implication.as.constraints.lemma}.

In the special case of logic programs a  model of ${\cal C}(P)$ can be
found by using the techniques for set constraint solving.
For example the technique of Heintze and Jaffar \shortcite{HJ90lics,HJ91}
produces 
a (non-discriminative) term grammar specifying the least model
of set constraints. This technique has been used for generating
approximations of logic program semantics %
\comment{PP:Dodaje HJ90popl i HJ94cpjak recenzent kazal.}
\cite{HJ90popl,Heintze92,HJ94cp,CP98}.
\comment{PP:uzupelniam nastepne zdanie o SAS97}
Another constraint solving approach that uses tree automata 
techniques, has been presented in 
\cite{DevienneTT97sas,TalbotDT2000}. 
We expect that these techniques can be generalized to the case
of CLP programs, but we did not investigate this
issue yet.
\comment{Bylo we wrzesniu
However, it has been pointed out by Heintze
that it is difficult to obtain acceptable efficiency of an
implementation of his constraint solving algorithms.
Therefore we leave the issue of generalizing the constraint solving
approaches as a topic of
future work and in our work we focus on another approach discussed below.
}
\comment{Poprzednie wersje i notatki

\comment{O cos nam tu chodzilo:\\
 In Section ... 
we sketch a rough  idea of such an extension.
\\
(czyli dolaczamy gdzie indziej - w rozdziale 4 ? sekcje
solving parametric constraints-
 cos w rodzaju zmodyfikowanej sekcji 3.1.3 gdzie wiezy  
 bez parametrow sa specjalnym przypadkiem ).
\\
Ale wyglada, ze tego nie zrobimy.

Nastepne zdanie trzeba wywazyc.
}
 However, it has been pointed out by Heintze
\cite{Heintze92}
\comment{ (tu dokladny cytat z podaniem strony)
that practical implementation
of his constraint solving algorithms may be rather difficult.

that the efficiency of practical implementations of his constraint
solving algorithms  is rather poor.
}
that it is difficult to obtain acceptable efficiency of an
implementation of his constraint solving algorithms.
This applies even more to the extension. Therefore we leave
the issue of implementation of the extension as a topic of
future work and in our work we focus on another approach discussed below.
}



Yet another approach to  finding a model of the constraint system 
${\cal C}(P)$  stems from abstract interpretation techniques
(among others \cite{JB92,HCC95}, \cite{GW94},
we generalize the latter work in
\cite{DrabentP99,DrabentMP99,DrabentMP00} and here). 
${\cal C}(P)$  is seen as a valuation transformer, its fixed points
are models of ${\cal C}(P)$.
Valuations are represented as discriminative grammars.
A fixed point is computed iteratively.  


To augment our system with a tool for computing approximations of program
semantics, we provide a
solution based on the latter idea.
This choice was guided mainly by possibility of reusing our
correctness checking algorithm
and the implementation of \cite{GW94}.


The correctness checking algorithm of the previous section can be
easily modified to compute the valuation transformer related to
${\cal C}(P)$.
This gives an implementation of a single step of
the iteration.  It remains to combine it with some technique of
assuring termination.

\medskip\noindent
\textbf{Iteration step.}
\
Take $G_i$ (initially $G_0$).
To each $ F'_j(C)  \cup G_i$ apply the construction as in the
correctness checking, obtaining a discriminative grammar $F_{C,j}$.
(It is required that all the obtained grammars have distinct variables,
except \Ca and \Su).
For each  $F_{C,j}$, the variables occurring in  $F_{C,j}$ are
distinct from those in $G_i$ except for \Ca or \Su.
\comment{
Nieprawda, ze: \ \ 
The least models of $ F'_j(C) \cup G_i$ and of
$F_{C,j}$ coincide on their common variables.
}

The constraints of  $F'_j(C)$ are satisfied if the occurrences of \Ca,
 \Su in the right hand side of each constraint of the form 
(\ref{implication.as.constraints1}) (Section \ref{section.ver.cond}) 
are valuated as in the least model
of $G_i$, and the remaining variable occurrences as in the least
model of  $F_{C,j}$.
This follows from the discussion in the previous section.
\comment{
   Mozna tez rozbic $F_{C,j}$ na czesci $G'$ i $G''$, jak w porzednim
   rozdziale,  i powiedziec, ze (1) sa spelnione w
   najmniejszym modelu  $G\cup G'$,  zas (2) w    $G'\cup G''$.
Ponizej, gdy mowimy o calym ${\cal C}(P)$, mozna to samo zrobic z  $G_{i+1}$.
}
\comment{
Chyba bez sensu: \\
Chyba wystarczy tylko $\gra[G_0]\Su$ zamiast $G_0$, ale to wymaga
dodatkowych wyjasnien.
}

The obtained grammar
 $G_i' = G_i\cup \bigcup_{C\in P} \bigcup_j  F_{C,j}$ is not discriminative,
due to the rules for \Ca and for \Su.
Construct a discriminative approximation of $G_i'$, more precisely a
discriminative grammar  $G_{i+1}$ such that
$\sem[G'_i]{\Ca}\subseteq\sem[G_{i+1}]{\Ca}$ and the same for \Su.
This is done by applying the union operation of
 Section~\ref{term-grammars}
to $G_i$ and all grammars $F_{C,j}$.
(So $G_{i+1}$ is
$G_i\mathop{\dot\cup} \dot{\bigcup}_{C\in P} \dot{\bigcup}_j  F_{C,j}$
with the variable $\Ca\dot\cup\ldots\dot\cup\Ca$ renamed into $\Ca$
and  $\Su\dot\cup\ldots\dot\cup\Su$ renamed into $\Su$.)
\comment{
To jest przyklad, jak pozornie potrzebna operacja zaokraglania do
discriminative grammars staje sie niepotrzebna
}

The obtained grammar $G_{i+1}$ has the following property.
${\cal C}(P) - G_0$ is true when  \Ca and \Su in
all the constraints of the form
(\ref{implication.as.constraints1}) (Section \ref{section.ver.cond}) 
are valuated as in the least model
of  $G_i$,
\Ca and \Su in the constraints of the form
(\ref{implication.as.constraints2}) (Section \ref{section.ver.cond})  
as in the least model of  $G_{i+1}$,
and the (renamed) variables of $P$ as in the least model of $G_i'$.
\comment{
Bylo: \ \ 
${\cal C}(P) - G_0$ is true when  \Ca and \Su in
all the constraints of the form
(\ref{implication.as.constraints1}) are valuated as in the least model
of  $G_i$
and all the other variable occurrences as in the least model of $G_i'$
(or in the least model of $G_{i+1}$).

I to w nawiasie jest nieprawda, w tej gramatyce nie wystepuja zmienne
z programu.  A chodzi nam o odniesienie do $G_{i+1}$.
}
\comment{
Bylo zle:
 ${\cal C}(P)$ is true when  \Ca and \Su in
(\ref{implication.as.constraints2}) are valuated as in the least model
of  $G_i'$ (or the least model of $G_{i+1}$)
and all the other variable occurrences as in the least model of $G_i$.
}
\comment{Another formulation, which is better?: \
There exists a ``solution'' of ${\cal C}(P)$ in which 
 \Ca and \Su in
(\ref{implication.as.constraints1}) are valuated as in the least model
\ldots
 and all the other variable occurrences as in \ldots
}

It remains to check whether the specification given by $G_{i+1}$
does not contain incorrect calls of constraint predicates.
  This boils down to checking whether 
all the calls of constraint predicates from the set
\sem[G_{i+1}]\Ca\ are also members of \sem[G_0]\Ca.
The latter is equivalent to
$\sem[F]\Ca\subseteq\sem[G_0]\Ca$,
where
$F = G_{i+1}-\{\,\Ca{>}A\mid A \mbox{ is not a constraint}\,\}$.
\comment{Mozna tez: \ \ 
$F = G_{i+1}-\{\,\Ca\mathop{>}p(\vec X)\mid
 p \mbox{ is not a constraint predicate}\,\}$.
}
Failure of the check means that we are unable to construct a
specification which respects constraints.  This suggests a program
error and an appropriate warning is issued.

This completes an iteration step.  Notice that the calls and successes
of constraint predicates
specified by $G_{i+1}$ are the same as those specified by $G_i$ and
thus by $G_0$ (induction on $i$).
For calls it follows from succeeding of the checks above.
For successes we have that
any clause $\Su\mathop>p(\vec X)$ from  $G_{i+1}$,
where $p$ is a constraint predicate,
occurs also in $G_i$.






The iteration is terminated if a fixpoint is reached, this means
when
$\sem[G_{i+1}]{\Ca} \subseteq \sem[G_i]{\Ca}$ and
$\sem[G_{i+1}]{\Su} \subseteq \sem[G_i]{\Su}$.
(The inclusion in the other direction holds for each $i$).
The required model of   ${\cal C}(P)$ is 
a valuation in which the values of the variables from $G_0$, except
for \Ca and \Su, are as in the least model of  $G_0$,
 the values of  \Ca, \Su are as in the least model of
$G_{i}$,
and the variables of $P$ are valuated by the least model of $G_i'$.
{\sloppy\par}

As a result we obtain that whenever the iteration terminates,
program $P$ is correct w.r.t.\ the
specification given by the obtained grammar $G_{i}$.

Notice that this is justified in a
different way than usually done in abstract interpretation.
Instead of relating a single iteration step to the concrete semantics
of the program, we showed that the obtained fixpoint satisfies  
a sufficient condition for program correctness.

\comment{Was: \ \ \
Such iterative techniques are usually justified without a reference to
set constraints or sufficient conditions for correctness.
Instead, the technique is seen as an instance of the abstract
interpretation paradigm.
The valuation transformer is shown to be correct w.r.t.\ a
function defining a fixpoint semantics of the program.  
Hence the fixpoint found approximates the program's semantics.
}



\medskip\noindent



\textbf{Termination.}
\
Usually the iterative process described above does not terminate.
It should be augmented with means of assuring termination.
The idea is to apply a {\em restriction} operator $\cal R$
that maps an infinite domain of grammars to its finite subset.
Moreover,
 the operator $\cal R$ 
computes an approximation of a grammar $G$ (i.e.\ $\sem[G]{\Ca} \subseteq \sem[{\cal R}(G)]{\Ca}$ and 
$\sem[G]{\Su} \subseteq \sem[{\cal R}(G)]{\Su}$).  
The operator is applied in every iteration step: the newly obtained
grammar $G_{i+1}$  
is replaced by a grammar  $H_{i+1} = {\cal R}(G_{i+1})$.
In this way we obtain a sequence of grammars $G_0, H_1, H_2, \ldots$,
the sequence has the properties described in the previous paragraphs.
Since the co-domain of $\cal R$ is finite, the set of grammars 
$\{\,G_0,  H_1, H_2, \ldots\,\}$ is finite and the iteration terminates.
This technique can be seen as an instance of widening
\cite{CousotJLP92}.

An attempt at such approach was made by Gallagher and de Waal  \shortcite{GW94}.
Unfortunately, the termination proof given by the authors is erroneous
and Mildner \shortcite{Mil99} showed an artificial example which
results in an infinite loop.





We adapt a technique
presented  in \cite{Mil99}, Section 6.5, and inspired by  \cite{JB92}.
We describe it briefly.
Let the {\em principal label} of a variable $X$ be the set of function symbols occurring in the 
right hand sides of the rules defining $X$ in a given grammar $G$. 
Let a {\em term grammar graph} be a directed graph with grammar  variables as vertices.
An edge $(X,Y)$ belongs to the graph iff there is a rule $X > f(\ldots,Y,\ldots)$ in the grammar.
The operator $\cal R$ 
computes an approximation of a grammar $G$ (\,$\sem[G]{\Ca} \subseteq \sem[{\cal R}(G)]{\Ca}$ and 
$\sem[G]{\Su} \subseteq \sem[{\cal R}(G)]{\Su}$) 
assuring at the same time that there is 
a spanning tree of the graph of ${\cal R}(G)$ such that
each branch of the tree contains no more than $k$
variables with the same principal label.
Since the grammar is discriminative, and
since there is a finite number of function symbols in a program,
the set of such spanning trees (modulo variable renaming), is finite
and consequently the co-domain of $\cal R$ (modulo variable
renaming) is finite.
We usually apply $k=1$.

 The reasoning above
 does not provide any useful estimation of
 the complexity of the algorithm.  Our experience shows that it is
 sufficiently efficient to compute directional types of
 medium size programs. 



There exist variants of this method, taking into account a number of occurrences of a 
single function symbol along a path or just simply binding a depth of the 
spanning tree with a constant.

Another possibility to cope with the termination problem is to restrict the class of grammars
so that the class of defined sets is a partial order 
of finite heights\footnote{For example Boye \shortcite{Boy96} suggested
that the inference is always done with a finite lattice of types.
In practice this means that for a class of applications we may 
have a finite library of types, represented by grammars, which
may be extended by need. This will also facilitate 
 communication with the user who will easier  understand standard
application-specific types than the types represented by automatically
generated grammars.}. 



















artcom.bbl
\begin{thebibliography}{}

\bibitem[\protect\citename{Aiken \& Lakshman, }1994]{AikenL94}
Aiken, A., \& Lakshman, T.~K. (1994).
\newblock Directional type checking of logic programs.
\newblock {\em Pages  43--60 of:} LeCharlier, B. (ed), {\em Proc. of the 1st
  {I}nt. {S}ymposium on {S}tatic {A}nalysis}.
\newblock LNCS, vol. 864.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Apt, }1993]{Apt93}
Apt, K.~R. (1993).
\newblock Declarative programming in {P}rolog.
\newblock {\em Pages  12--35 of:} Miller, D. (ed), {\em Proccedings of the
  {I}nternational {S}ymposium on {L}ogic {P}rogramming}.
\newblock The MIT Press.

\bibitem[\protect\citename{Apt, }1997]{Apt97}
Apt, K.~R. (1997).
\newblock {\em {From Logic Programming to {P}rolog}}.
\newblock Prentice Hall.

\bibitem[\protect\citename{Bossi \& Cocco, }1989]{BC89}
Bossi, A., \& Cocco, N. (1989).
\newblock Verifying correctness of logic programs.
\newblock {\em Pages  96--110 of:} D{\'\i}az, J., \& Orejas, F. (eds), {\em
  Proceedings of the {I}nternational {J}oint {C}onference on {T}heory and
  {P}ractice of {S}oftware {D}evelopment {TAPSOFT}~'89}.
\newblock LNCS, vol. 352.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Boye, }1996]{Boy96}
Boye, J. (1996).
\newblock {\em {Directional Types in Logic Programming}}.
\newblock Link\"oping studies in science and technology, dissertation no. 437,
  Link\"oping University.

\bibitem[\protect\citename{Boye \& Ma{\l}uszy\'nski, }1997]{BM97}
Boye, J., \& Ma{\l}uszy\'nski, J. (1997).
\newblock Directional types and the annotation method.
\newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 33}(3), 179--220.

\bibitem[\protect\citename{Bronsard {\em et~al.}\relax, }1992]{BLR92}
Bronsard, F., Lakshman, T.~K., \& Reddy, U. (1992).
\newblock A framework of directionality for proving termination of logic
  programs.
\newblock {\em Pages  321--335 of:} Apt, K.~R. (ed), {\em Proceedings of the
  {J}oint {I}nternational {S}ymposium and {C}onference on {L}ogic
  {P}rogramming}.
\newblock The MIT Press.

\bibitem[\protect\citename{Bueno {\em et~al.}\relax, }1997]{BuenoDDFHMP97}
Bueno, F., Deransart, P., Drabent, W., Ferrand, G., Hermenegildo, M.,
  Ma{\l}uszy\'nski, J., \& Puebla, G. (1997).
\newblock On the role of semantic approximations in validation and diagnosis of
  constraint logic programs.
\newblock {\em Pages  155--169 of:} Kamkar, M. (ed), {\em Proceedings of the
  {AADEBUG}'97 ({T}he {T}hird {I}nternational {W}orkshop on {A}utomated
  {D}ebugging)}.
\newblock Link{\"o}ping University.

\bibitem[\protect\citename{Charatonik, }1998]{Charatonik98ic}
Charatonik, W. (1998).
\newblock Set constraints in some equational theories.
\newblock {\em Information and computation}, {\bf 142}(1), 40--75.

\bibitem[\protect\citename{Charatonik \& Podelski, }1997]{CharatonikP97lics}
Charatonik, W., \& Podelski, A. (1997).
\newblock Set constraints with intersection.
\newblock {\em Pages  362--372 of:} Winskel, Glynn (ed), {\em {Twelfth Annual
  IEEE Symposium on Logic in Computer Science}}.

\bibitem[\protect\citename{Charatonik \& Podelski, }1998]{CP98}
Charatonik, W., \& Podelski, A. (1998).
\newblock Directional type inference for logic programs.
\newblock  Levi, G. (ed), {\em Proceedings of the 5th static analysis symposium
  ({SAS}'98)}.
\newblock LNCS, vol. 1503.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Comini {\em et~al.}\relax, }1998]{DeliverCDMP98}
Comini, M., Drabent, W., Ma{\l}uszy\'nski, J., \& Pietrzak, P. (1998).
\newblock {\em A type-based diagnoser for {CHIP}}.
\newblock {ESPRIT} {DiSCiPl} deliverable.
\newblock Available at URL:
  {\texttt{http://discipl.inria.fr/deliverables2.html}}.

\bibitem[\protect\citename{Comini {\em et~al.}\relax, }1999]{CominiDP99gulp}
Comini, M., Drabent, W., \& Pietrzak, P. (1999).
\newblock {Diagnosis of CHIP Programs Using Type Information}.
\newblock {\em Pages  337--349 of:} Meo, M.~C., \& Vilares~Ferro, M. (eds),
  {\em {APPIA-GULP-PRODE'99, Joint Conference on Declarative Programming}}.

\bibitem[\protect\citename{Comini {\em et~al.}\relax, }2000]{CominiGLV99entcs}
Comini, M., Gori, R., Levi, G., \& Volpe, P. (2000).
\newblock {Abstract Interpretation based Verification of Logic Programs}.
\newblock  Etalle, S., \& Smaus, J.-G. (eds), {\em Proceedings of the workshop
  on verification of logic programs}.
\newblock Electronic Notes in Theoretical Computer Science, vol. 30.
\newblock Elsevier Science Publishers.
\newblock Available at URL:
  {\texttt{http://www.elsevier.nl/locate/entcs/volume30.html}}.

\bibitem[\protect\citename{Comon {\em et~al.}\relax, }1997]{TATA}
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., \&
  Tommasi, M. (1997).
\newblock {\em Tree automata techniques and applications}.
\newblock Available on: {\tt http://www.grappa.univ-lille3.fr/tata}.

\bibitem[\protect\citename{Cosytec, }1998]{CHIP}
Cosytec. (1998).
\newblock {\em {CHIP} system documentation}.

\bibitem[\protect\citename{Cousot \& Cousot, }1992]{CousotJLP92}
Cousot, P{.}, \& Cousot, R{.} (1992).
\newblock Abstract interpretation and application to logic programs.
\newblock {\em Journal of logic programming}, {\bf 13}(2--3), 103--179.
\newblock {\footnotesize (For a correct version of this paper, see {\tt
  http://www.di.ens.fr/\~{}cousot}.)}.

\bibitem[\protect\citename{Dart \& Zobel, }1992]{DZ92}
Dart, P., \& Zobel, J. (1992).
\newblock {A regular type language for logic programs}.
\newblock {\em Pages  157--187 of:} Pfenning, F. (ed), {\em Types in {L}ogic
  {P}rogramming}.
\newblock The MIT Press.

\bibitem[\protect\citename{Deransart, }1993]{Der93}
Deransart, P. (1993).
\newblock Proof methods of declarative properties of definite programs.
\newblock {\em {Theoretical {C}omputer {S}cience}}, {\bf 118}, 99--166.

\bibitem[\protect\citename{Deransart \& Smaus, }2001]{DeransartS01}
Deransart, P., \& Smaus, J.-G. (2001).
\newblock Well-typed logic programs are not wrong.
\newblock {\em Pages  280--295 of:} H.~Kuchen, K.~Ueda (ed), {\em Functional
  and logic programming ({FLOPS'2001})}.
\newblock LNCS, no.  2024.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Devienne {\em et~al.}\relax,
  }1997a]{DevienneTT97sas}
Devienne, P., J.-M., Talbot, \& Tison, S. (1997a).
\newblock Set-based analysis for logic programming and tree automata.
\newblock {\em Pages  127--140 of:} {\em {Proceedings of the Static Analysis
  Symposium, SAS'97}}.
\newblock LNCS, vol. 1302.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Devienne {\em et~al.}\relax, }1997b]{DevienneTT97cp}
Devienne, P., Talbot, J.-M., \& Tison, S. (1997b).
\newblock Solving classes of set constraints with tree automata.
\newblock {\em Pages  62--76 of:} Smolka, Gert (ed), {\em {Proceedings of the
  Third International Conference on Principles and Practice of Constraint
  Programming - CP97}}.
\newblock LNCS, vol. 1330.
\newblock Berlin, Germany: Springer-Verlag.

\bibitem[\protect\citename{Drabent \& Ma{\l}uszy\'nski, }1988]{DM88a}
Drabent, W., \& Ma{\l}uszy\'nski, J. (1988).
\newblock Inductive assertion method for logic programs.
\newblock {\em Theoretical {C}omputer {S}cience}, {\bf 59}(1), 133--155.

\bibitem[\protect\citename{Drabent \& Pietrzak, }1998]{DeliverDP98}
Drabent, W., \& Pietrzak, P. (1998).
\newblock {\em Inferring call and success types for {CLP} programs}.
\newblock {ESPRIT} {DiSCiPl} deliverable.
\newblock Available at URL:
  {\texttt{http://discipl.inria.fr/deliverables2.html}}.

\bibitem[\protect\citename{Drabent \& Pietrzak, }1999]{DrabentP99}
Drabent, W., \& Pietrzak, P. (1999).
\newblock {Type Analysis for CHIP}.
\newblock {\em Pages  389--405 of:} Haeberer, A.M. (ed), {\em Proc. of the
  {S}eventh {I}nternational {C}onference on {A}lgebraic {M}ethotology and
  {S}oftware {T}echnology ({AMAST}'98)}.
\newblock LNCS, vol. 1548.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Drabent {\em et~al.}\relax, }2000a]{DrabentMP00}
Drabent, W., Ma{\l}uszy\'nski, J., \& Pietrzak, P. (2000a).
\newblock Locating {T}ype {E}rrors in {U}ntyped {CLP} {P}rograms.
\newblock {\em Chap. 4, pages  121--150 of:} Hermenegildo, M., Deransart, P.,
  \& Ma{\l}uszy\'nski, J. (eds), {\em Analysis and {V}isualization {T}ools for
  {C}onstraint {P}rogramming}.
\newblock LNCS, vol. 1870.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Drabent {\em et~al.}\relax, }2000b]{DrabentMP99}
Drabent, W., Ma{\l}uszy\'nski, J., \& Pietrzak, P. (2000b).
\newblock {T}ype-based {D}iagnosis of {CLP} {P}rograms.
\newblock  Mireille~Ducass�, Anthony~Kusalik, \& Puebla, German (eds), {\em
  {WLPE'99, Tenth Workshop on Logic Programming Environments}}.
\newblock Electronic {N}otes in {T}heoretical {C}omputer {S}cience, vol. 30,
  no. ~4.
\newblock Elsevier Science Publishers.
\newblock Available at URL:
  {\texttt{http://www.elsevier.nl/locate/entcs/volume30.html}}.

\bibitem[\protect\citename{Drabent {\em et~al.}\relax, }2001]{DrabentMP01paris}
Drabent, W., Ma{\l}uszy\'nski, J., \& Pietrzak, P. (2001).
\newblock Parametric descriptive types for {(C)LP}.
\newblock {\em Pages  239--254 of:} Codognet, P. (ed), {\em {The Tenth
  International French Speaking Conference on Logic and Constraint
  Programming}}.
\newblock Paris: Hermes-Science.

\bibitem[\protect\citename{Fages \& Coquery, }2001]{FagesC01}
Fages, F., \& Coquery, E. (2001).
\newblock Typing constraint logic programs.
\newblock {\em Theory and practice of logic programming}, {\bf 1}(6), 751--777.

\bibitem[\protect\citename{Fr\"uhwirth {\em et~al.}\relax, }1991]{FSVY91}
Fr\"uhwirth, T., Shapiro, E., Vardi, M., \& Yardeni, E. (1991).
\newblock Logic programs as types for logic programs.
\newblock {\em Pages  300--309 of:} Kahn, G. (ed), {\em Annual {IEEE}
  {S}ymposium on {L}ogic in {C}omputer {S}cience}.
\newblock Corrected version available from
  \texttt{http://WWW.pst.informatik.uni-muenchen.de/\~{}fruehwir}.

\bibitem[\protect\citename{Gallagher \& de~Waal, }1994]{GW94}
Gallagher, J., \& de~Waal, D.~A. (1994).
\newblock Fast and precise regular approximations of logic programs.
\newblock {\em Pages  599--613 of:} Hentenryck, P.~Van (ed), {\em {Proc.~of the
  Eleventh International Conference on Logic Programming}}.
\newblock The MIT Press.

\bibitem[\protect\citename{Heintze, }1992]{Heintze92}
Heintze, N. (1992).
\newblock Practical aspects of set based analysis.
\newblock {\em Pages  765--779 of:} Apt, M. (ed), {\em {Proceedings of the
  Joint International Conference and Symposium on Logic Programming }}.
\newblock The MIT Press.

\bibitem[\protect\citename{Heintze \& Jaffar, }1990a]{HJ90lics}
Heintze, N., \& Jaffar, J. (1990a).
\newblock A decision procedure for a class of set constraints (extended
  abstract).
\newblock {\em Pages  42--51 of:} {\em {Fifth Annual IEEE Symposium on Logic in
  Computer Science}}.

\bibitem[\protect\citename{Heintze \& Jaffar, }1990b]{HJ90popl}
Heintze, N., \& Jaffar, J. (1990b).
\newblock A finite presentation theorem for approximating logic programs.
\newblock {\em Pages  197--209 of:} {\em {Seventeenth Annual {ACM} Symposium on
  Principles of Programming Languages}}.

\bibitem[\protect\citename{Heintze \& Jaffar, }1991]{HJ91}
Heintze, N., \& Jaffar, J. (1991).
\newblock {\em {A Decision Procedure for a Class of Set Constraints}}.
\newblock Tech. rept. CMU-CS-91-110. Carnegie Mellon University.

\bibitem[\protect\citename{Heintze \& Jaffar, }1994]{HJ94cp}
Heintze, N., \& Jaffar, J. (1994).
\newblock Set constraints and set-based analysis.
\newblock {\em Pages  281--298 of:} {\em {Proceedings of the Workshop on
  Principles and Practice of Constraint Programming}}.
\newblock LNCS, vol. 874.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Hill \& Lloyd, }1994]{HL94}
Hill, P.M., \& Lloyd, J.W. (1994).
\newblock {\em {The G{\"o}del Programming Language}}.
\newblock The MIT Press.

\bibitem[\protect\citename{Hopcroft {\em et~al.}\relax, }2001]{HopcroftU01}
Hopcroft, J.~E., Motwani, R., \& Ullman, J.~D. (2001).
\newblock {\em Introduction to {A}utomata {T}heory, {L}anguages and
  {C}omputation}. 2 edn.
\newblock Addison-Wesley.

\bibitem[\protect\citename{Janssens \& Bruynooghe, }1992]{JB92}
Janssens, G., \& Bruynooghe, M. (1992).
\newblock {Deriving descriptions of possible values of program variables by
  means of abstract interpretation}.
\newblock {\em {Journal of Logic Programming}}, {\bf 13}(2 \& 3), 205--258.

\bibitem[\protect\citename{Lloyd, }1987]{Lloyd87}
Lloyd, J.~W. (1987).
\newblock {\em {Foundations of Logic Programming}}. Second, extended edn.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Mildner, }1999]{Mil99}
Mildner, P. (1999).
\newblock {\em Type domains for abstract interpretation, a critical study}.
\newblock Ph.D. thesis, Uppsala University.

\bibitem[\protect\citename{Mishra, }1984]{Mis84}
Mishra, P. (1984).
\newblock Towards a theory of types in {Prolog}.
\newblock {\em Pages  289--298 of:} {\em {Proceedings of the IEEE International
  Symposium on Logic Programming}}.

\bibitem[\protect\citename{Mycroft \& O'Keefe, }1984]{MycroftK84}
Mycroft, A., \& O'Keefe, R.~A. (1984).
\newblock {A Polymorphic Type System for {P}rolog}.
\newblock {\em {Artificial Intelligence}}, {\bf 23}, 295--307.

\bibitem[\protect\citename{Puebla {\em et~al.}\relax, }2000]{PueblaBH00}
Puebla, G., Bueno, F., \& Hermenegildo, M. (2000).
\newblock A {G}eneric {P}reprocessor for {P}rogram {V}alidation and
  {D}ebugging.
\newblock {\em Chap. 2, pages  63--107 of:} Hermenegildo, M., Deransart, P., \&
  Ma{\l}uszy\'nski, J. (eds), {\em Analysis and {V}isualization {T}ools for
  {C}onstraint {P}rogramming}.
\newblock LNCS, vol. 1870.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Rychlikowski \& Truderung, }2000]{RT00}
Rychlikowski, P., \& Truderung, T. (2000).
\newblock {\em Polymorphic directional types for logic programming}.
\newblock Ph.D. thesis, Wroc{\l}aw University.
\newblock
  \texttt{http://www.tcs.uni.wroc.pl/\~{}tt/\linebreak[3]dirtypes/index.html}.

\bibitem[\protect\citename{Rychlikowski \& Truderung, }2001]{RTppdp01}
Rychlikowski, P., \& Truderung, T. (2001).
\newblock Polymorphic directional types for logic programming.
\newblock {\em Pages  61--72 of:} {\em Proceedings of the 3rd international
  {ACM SIGPLAN} conference on principles and practice of declarative
  programming}.
\newblock ACM Press.

\bibitem[\protect\citename{SICS, }1998]{sicstus}
SICS. (1998).
\newblock {\em {SICS}tus {Prolog} user's manual}.
\newblock Intelligent Systems Laboratory.

\bibitem[\protect\citename{Smaus {\em et~al.}\relax, }2000]{SmausFD00}
Smaus, J.-G., Fages, F., \& Deransart, P. (2000).
\newblock Using modes to ensure subject reduction for typed logic programs with
  subtyping.
\newblock {\em Pages  214--226 of:} S.~Kapoor, S.~Prasad (ed), {\em Foundations
  of software technology and theoretical computer science ({FST TCS'2000})}.
\newblock LNCS, no.  1974.
\newblock Springer-Verlag.

\bibitem[\protect\citename{Somogyi {\em et~al.}\relax, }1996]{SHC96}
Somogyi, Z., Henderson, F., \& Conway, T. (1996).
\newblock {The execution algorithm of Mercury: an efficient purely declarative
  logic programming language}.
\newblock {\em {Journal of Logic Programming}}, {\bf 29}(1--3), 14--64.

\bibitem[\protect\citename{Talbot {\em et~al.}\relax, }2000]{TalbotDT2000}
Talbot, J.-M., Devienne, P., \& Tison, S. (2000).
\newblock Generalized definite set constraints.
\newblock {\em {Constraints: An International Journal}}, {\bf 5}(1-2),
  161--202.

\bibitem[\protect\citename{Van~Hentenryck, }1989]{Hen89}
Van~Hentenryck, P. (1989).
\newblock {\em {Constraint Satisfaction in Logic Programming}}.
\newblock The MIT Press.

\bibitem[\protect\citename{Van~Hentenryck {\em et~al.}\relax, }1995]{HCC95}
Van~Hentenryck, P., Cortesi, A., \& Charlier, B.~Le. (1995).
\newblock Type analysis of {Prolog} using type graphs.
\newblock {\em Journal of logic programming}, {\bf 22}(3), 179--209.

\bibitem[\protect\citename{Yardeni \& Shapiro, }1991]{YS91}
Yardeni, E., \& Shapiro, E.~Y. (1991).
\newblock {A type system for logic programs}.
\newblock {\em {Journal of Logic Programming}}, {\bf 10}(2), 125--153.

\bibitem[\protect\citename{Zobel, }1987]{Zobel87}
Zobel, J. (1987).
\newblock Derivation of polymorphic types for {P}rolog programs.
\newblock {\em Pages  817--838 of:} Lassez, J-L. (ed), {\em {Proceedings of the
  Fourth International Conference on Logic Programming}}.
\newblock The {MIT} Press.

\end{thebibliography}
