We present a goal-independent abstract interpretation framework for constraint logic programs, and prove the sufficiency of a set of conditions for abstract domains to ensure that the analysis will never lose precision. Along the way, we formally define constraint logic programming systems, give a formal semantics that is independent of the actual constraint domain and the details of the proof algorithm, and formally define the maximally precise abstraction of a constraint logic program.
展开▼
