Warp wrote:
>   Given that in a Turing-complete language it's impossible to prove
> in the generic case whether a certain piece of code is ever executed
> or not, that would mean that the language would have to be less
> expressive than a Turing machine.

I think you're overgeneralizing. Is it not possible to prove that you 
never use a variable before you assign to it, or that every path to exit 
a value-returning-function actually returns a value? Of course it is. 
Why is it harder to prove you never read from a file handle after it has 
hit EOF?

You might not be able to tell whether a program *will* get to any 
particular point in the code, but you can certainly make it illegal for 
it to get to particular places in the code and hence guarantee it does 
*not* get to that point.

Every implementation of typestate I've seen where people rely on it 
(i.e., require the semantics for the language to work, rather than just 
issuing warnings) includes annotations on module-spanning APIs. In other 
words, when you open a file, the returned file handle is marked at 
"open", and when you read the EOF, it's actually an exception (meaning 
the execution returns to a different place in the code rather than 
returning a flag), so it's easy to tell at each particular line in the 
code whether a file is open or not. I.e., if you have a function that 
returns a file handle, you have to say whether that file handle is 
already at EOF or not, for example.

It also rules out constructs like
   int z;
   if (x == y)
      z = 0;
   my_func(z);

That doesn't make it less turing complete.
-- 
Darren New / San Diego, CA, USA (PST)

Post a reply to this message