Changes

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.

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

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

| url = jjc.public.iastate.edu/Runtime.errors.Paper.March4.2006.pdf

| title = A Survey of Systems for Detecting Serial Run-Time Errors

| title = A Survey of Systems for Detecting Serial Run-Time Errors

| author = Glenn R. Luecke et al

| 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.

| 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

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

| url = http://www.schneier.com/blog/archives/2009/10/proving_a_compu.html

| title = Proving a Computer Program's Correctness

| title = Proving a Computer Program's Correctness

| author = Bruce Schneier

| 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

| 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

| url = www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh.../chapter7.ps.gz

| title = Hoare Logic: Proving Programs Correct

| title = Hoare Logic: Proving Programs Correct

| author = Jonathan Aldrich

| author = Jonathan Aldrich

| accessdate = 2012-04-03}}</ref>

| accessdate = 2012-04-03}}

</ref>

==Optimisation==

==Optimisation==