SkipCaptcha
265
edits
Changes
Jump to navigation
Jump to search
Line 78:
Line 78: + + + + + + + + + + + + + + + + + +
→Dealing with errors: detecting run-time errors; proving programs correct
During translation compilers can usually detect all errors due to lexical or syntactical mistakes (spelling and grammar); they may also be able to detect a few simple semantic errors (meaning). Even when a compiler does detect and report an error, all it can do is report what the error is and where it was detected; unfortunately the point of detection can be in some cases be many lines away from the actual source of the error; also it may be difficult to explain the error in terms that the programmer can understand.
During translation compilers can usually detect all errors due to lexical or syntactical mistakes (spelling and grammar); they may also be able to detect a few simple semantic errors (meaning). Even when a compiler does detect and report an error, all it can do is report what the error is and where it was detected; unfortunately the point of detection can be in some cases be many lines away from the actual source of the error; also it may be difficult to explain the error in terms that the programmer can understand.
A semantic/coding error such as using a plus sign '+' instead of a minus sign '-' is almost impossible for any automated system to detect - thorough human checking of both code and calculated results would be needed in this situation.
There are a wide variety of errors which can occur when a program is running.<ref>{{cite web
| url = jjc.public.iastate.edu/Runtime.errors.Paper.March4.2006.pdf
| title = A Survey of Systems for Detecting Serial Run-Time Errors
| author = Glenn R. Luecke et al
| accessdate = 2012-04-03}}</ref> Some compilers can optionally generate extra code to check for many of these errors, and there are some software packages which can provide the same effect. Unfortunately this extra checking code can slow a program down by a factor of 10 or 20 times.
Research is continuing on the problem of proving that a program is correct. This is an extremely difficult problem - it has been shown that proving whether or not a program actually stops is [[undecidable]]. Furthermore the proofs are often a lot longer than the programs being proved so there is the additional problem of checking that the proof itself is correct. Bruce Schneier reports<ref>{{cite web
| url = http://www.schneier.com/blog/archives/2009/10/proving_a_compu.html
| title = Proving a Computer Program's Correctness
| author = Bruce Schneier
| accessdate = 2012-04-03}}</ref> that it took six people working for five years to prove the correctness of 7,500 line program (about 250 lines per man-year). Jonathan Aldrich provides some examples of proof methods applied to tiny programs.<ref>{{cite web
| url = www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh.../chapter7.ps.gz
| title = Hoare Logic: Proving Programs Correct
| author = Jonathan Aldrich
| accessdate = 2012-04-03}}</ref>
==Optimisation==
==Optimisation==