Mode checking using constrained regular trees
Lee Naish
In a previous paper we presented a high level polymorphic mode system
for logic programs. In this paper we present an algorithm which checks
if a program is well moded, given that is it well-typed in the sense of
Mycroft and O'Keefe. A program is well-moded if the set
of ground atoms defined by mode declarations is a superset of the
success set. The novelty of
the algorithm is the expressiveness of the mode declarations.
Constrained regular trees are used to define sets of terms and
atoms.
These are based on polymorphic types but allow set and multiset
constraints over type variables.
The expressiveness of this domain makes it very promising for many
program analysis applications.
Complexity is also (exponentially) better than other proposed domains
for certain analysis tasks.
Keywords:
logic programming, modes, types,
constrained regular trees, aliasing, linearity, set constraints,
multisets
Lee