The effectiveness of a type-checking tool strongly depends on the accuracy of the positional information that is associated with type errors. We present an approach where the location associated with an error message e is defined as a slice P e of the program P being type-checked. We show that this approach yields highly accurate positional information: P e is a program that contains precisely those program constructs in P that caused error e . Semantically, we have the interesting property that type-checking P e is guaranteed to produce the same error e . Our approach is completely language-independent and has been implemented for a significant subset of Pascal. We also report on experiments with object-oriented type systems, and with a subset of ML.

PIM is an equational logic designed to function as a “transformational toolkit” for compilers and other programming tools that analyze and manipulate imperative languages. It has been applied to such problems as program slicing, symbolic evaluation, conditional constant propagation, and dependence analysis. PIM consists of the untyped lambda calculus extended with an algebraic data type that characterizes the behavior of lazy stores and generalized conditionals. A graph form of PIM terms is by design closely related to several intermediate representations commonly used in optimizing compilers. In this article, we show that PIM's core algebraic component, PIM t , possesses a complete equational axiomatization (under the assumption of certain reasonable restrictions on term formation). This has the practical consequence of guaranteeing that every semantics-preserving transformation on a program representable in PIM t can be derived by application of PIM t rules. We systematically derive the complete PIM t logic as the culmination of a sequence of increasingly powerful equational systems starting from a straightforward “interpreter” for closed PIM t terms. This work is an intermediate step in a larger program to develop a set of well-founded tools for manipulation of imperative programs by compilers and other systems that perform program analysis.