What is a type error? [correction]

[Darren New]

David Hopwood wrote:
> Darren New wrote:
> 
>>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.
> 
> 
> Apparently, Hermes (at least the version of it described in that paper)
> essentially forgets that is_last has been initialized at the top of the
> loop, and so when it does the merge, it is merging 'not necessarily initialized'
> with 'initialized'.


No, it's not that it "forgets". It's that the "insert line into inputs" 
unitializes "line". Hence, "line" is only conditionally set at the 
bottom of the loop, so it's only conditionally set at the top of the loop.

> This sounds like a pretty easy thing to fix to me (and maybe it was fixed
> later, since there are other papers on Hermes' typestate checking that I
> haven't read yet).

You simply misunderstand the "insert line into inputs" semantics. Had 
that line actually been commented out in the Hermes code, the loop would 
have compiled without a problem.

That said, in my experience, finding this sort of typestate error 
invariably led me to writing clearer code.

boolean found_ending = false;
while (!found_ending) {
   string line = getString();
   if (line.charAt(0) == 'q')
     found_ending = true;
   else
     insert line into inputs;
}

It seems that's much clearer to me than the contorted version presented 
as the example. If you want it to work like the Java code, where you can 
still access the "line" variable after the loop, the rearrangement is 
trivial and transparent as well.

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