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.
--
http://mail.python.org/mailman/listinfo/python-list
