What is a type error?

[David Hopwood]

Darren New wrote:
> From what I can determine, the authors seem to imply that typestate is
> dataflow analysis modified in (at least) two ways:
> 
> 1) When control flow joins, the new typestate is the intersection of
> typestates coming into the join, where as dataflow analysis doesn't
> guarantee that. (They imply they think dataflow analysis is allowed to
> say "the variable might or might not be initialized here", while
> typestate would ensure the variable is uninitialized.)

Right, but this is a disadvantage of their typestate algorithm. It is why
the example in Figure 2 of
<http://www.cs.ubc.ca/local/reading/proceedings/spe91-95/spe/vol25/issue4/spe950wk.pdf>
fails to check, even though it "obviously" initializes all variables.

Consider the equivalent Java program:

public class LoopInitTest {
    public static void main(String[] args) {
        boolean b;
        int i;

        while (true) {
            b = true;
            if (b) {
                v = 1;
            }
            v = v + 1;
        }
    }
}

As it happens, javac rejects this:

LoopInitTest.java:12: variable v might not have been initialized
            v = v + 1;
                ^

but for a different and more trivial reason than the Hermes algorithm.
Change "if (b) { v = 1; }" to just "v = 1;", and the Java version will be
accepted by its definite assignment analysis (which is a dataflow analysis),
but the equivalent Hermes program still would not.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>