Im Artikel <7f812v$207...@news.gate.net>, "Joe \"Nuke Me Xemu\" Foster"
<j...@bftsi0.UUCP> schreibt:
Quote
>I think the conflict here is over terminology.
Agreed.
Can you please define a 'correct program'?
I only found the definition "conforms to the specifications", and some related
keywords like Reliability, Integrity and Completeness.
Quote
>>Optimizing code is a different topic, isn't it?
>Hang on a sec, Martin's not talking about code optimization here.
>He's using US terminology having to do with verifying things that
>should remain true both before and after a computation. Loop
>invariants are properties that should remain true even during the
>computation.
A code optimizer can determine the structure of existing code, and create the
conditions from that code. Then it can e.g. find loop invariants, based on
these conditions, and rearrange the code for better performance. Since an
optimizer doesn't modify the overall behaviour of a program, I considered loop
invariants as a topic of optimization, not of correctness.
Quote
>> However, I do think
that some good has come out of the program-proofs crowd.<<
Agreed.
The intention of the early high level languages mainly was to ease the
translation of algorithms into executable code (Algol, Fortran...). The next
language generation added more tags and structures to the languages, like
'const', 'loop', data types, classes etc., that did not only simplify the
process of translating the algorithms into procedures, but also added more
abstract information and conditions to the code, so that the compiler could
detect more common mistakes. Where Basic or Fortran code contained lots of
GoTo's, the newer languages implemented structural statements, that allowed to
convert the former spaghetti code into structured code. (Though IMO a GoTo in
the right place sometimes can reduce the amount of code, even nowadays ;-)
The next generation of programming languages should include a further (more
abstract) description of the algorithms and conditions, that are to be
implemented in the code. Then the compiler itself could prove the correctness
of the code, far beyond what's possible with encapsulation in the currently
used OO languages.
Quote
>>it's been proven that there can be no
program that can determine whether every possible loop even stops<<
But in contrast to the halting problem, a program can at least verify that the
program *can* eventually stop, and that the according conditions *can* be met
somehow.
DoDi