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. There's a company already doing that: http://www.praxis-his.com/sparkada/intro.asp Unfortunately the language is rather limited in terms of dynamic, hard-to-prove constructs like exceptions, pointers or gotos. For the ones who are interested, according to Lockheed: - Code quality improved by a factor of 10 over industry norms for DO 178B Level A software. - Productivity improved by a factor of 4 over previous comparable programs. - Development costs half of that typical for non safety-critical code. -- http://www.praxis-his.com/sparkada/pdfs/spark_c130j.pdf The most interesting sentence is probably the last. Doing it correct right from the start is actually cheaper. Vinzent. _______________________________________________ fpc-pascal maillist - fpc-pascal@lists.freepascal.org http://lists.freepascal.org/mailman/listinfo/fpc-pascal
