Op Tue, 14 Aug 2007, schreef Vinzent Hoefler:
> On Tuesday 14 August 2007 06:14, Daniël Mantione wrote:
>
> > Lastly, pre and post conditions are just another runtime check.
>
> No. If you can prove that the conditions always hold, you don't even
> need to compile to the program to prove its correctness.
This isn't feasible. Read on the internet about the Hoare calculus and
how is only feasible to do it for small programs. However, those programs
aren't a problem to get correct anyway.
There is no realistic way you can prove that a program like FPC itself is
correct.
Daniël
_______________________________________________
fpc-pascal maillist - fpc-pascal@lists.freepascal.org
http://lists.freepascal.org/mailman/listinfo/fpc-pascal
