Changes

There are a wide variety of errors which can occur when a program is running.<ref>

There are a wide variety of errors which can occur when a program is running.<ref>

{{cite web

{{cite web

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

| url=http://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}}

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

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

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

{{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}}

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

<ref>

{{cite web

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