On Tuesday 14 August 2007 06:49, Daniël Mantione wrote: > 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.
Ok. I'll tell Rod what his company is doing for years now, just ain't possi^Wfeasible. ;) Of course, you won't have much success with a language like Object Pascal, but I'd suggest reading a bit about SPARK before. And yes, FPC as it is is unprovable (first through all the language constructs used and second the problem most projects will suffer from: it isn't written with proving it in mind). OTOH, AFAIK, the correctness of the SPARK Examiner is proven. And those are a little bit more than just a dozen lines of code. Of course, it goes nowhere near a couple of millions of lines of code, but FPC does neither, if you just talk about the compiler. And correctness of stuff like the RTL can be proven independently from the compiler itself. Vinzent. _______________________________________________ fpc-pascal maillist - fpc-pascal@lists.freepascal.org http://lists.freepascal.org/mailman/listinfo/fpc-pascal
