What is a type error? [correction]

[Darren New]

David Hopwood wrote:
> 
> public class LoopInitTest {
>     public static String getString() { return "foo"; }
> 
>     public static void main(String[] args) {
>         String line = getString();
>         boolean is_last = false;
> 
>         while (!is_last) {
>             if (line.charAt(0) == 'q') {
>                 is_last = true;
>             }
> 
>             // insert line into inputs (not important for analysis)
> 
>             if (!is_last) {
>                 line = getString();
>             }
>         }
>     }
> }
> 
> which compiles without error, because is_last is definitely initialized.

At what point do you think is_last or line would seem to not be 
initialized? They're both set at the start of the function, and (given 
that it's Java) nothing can unset them.

At the start of the while loop, it's initialized. At the end of the 
while loop, it's initialized. So the merge point of the while loop has 
it marked as initialized.

Now, if the "insert line into inputs" actually unset "line", then yes, 
you're right, Hermes would complain about this.

Alternately, if you say
    if (x) v = 1;
    if (x) v += 1;
then Hermes would complain when it wouldn't need to. However, that's 
more a limitation of the typestate checking algorithms than the concept 
itself; that is to say, clearly the typestate checker could be made 
sufficiently intelligent to track most simple versions of this problem 
and not complain, by carrying around conditionals in the typestate 
description.

-- 
   Darren New / San Diego, CA, USA (PST)
     This octopus isn't tasty. Too many
     tentacles, not enough chops.