|
![](/i/fill.gif) |
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
|
![](/i/fill.gif) |