Dynamic determinacy analysis
Max Schäfer, Manu Sridharan, et al.
PLDI 2013
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 Pe of the program P being type checked. We show that this approach yields highly accurate positional information: Pe is a program that contains precisely those program constructs in P that caused error e. Semantically, we have the interesting property that type checking Pe is guaranteed to produce the same error e. Our approach is completely language-independent, and has been implemented for a significant subset of Pascal.
Max Schäfer, Manu Sridharan, et al.
PLDI 2013
Xiaoxia Ren, Barbara G. Ryder, et al.
ICSE 2005
Julian Dolby, Christian Hammer, et al.
ACM TOPLAS
Daniel Wasserrab, Tobias Nipkow, et al.
OOPSLA 2006