Menu
Independent of how sophisticated such testing is, empirical methods do not actually prove that a respective program is correct. The only thing we can actually prove with an empirical approach is that the program is incorrect - as a single example of incorrect behavior suffices.
SOFTWARE QUALITY FACTORS There are many schools of thought on what constitutes a complete set of factors, however this paper will cover the three we have already touched upon; Correctness, Efficiency and Understandability, along with Maintainability, Timeliness, Robustness, Reusability and Portability.
Computer programming is important today because so much of our world is automated. Humans need to be able to control the interaction between people and machines. Since computers and machines are able to do things so efficiently and accurately, we use computer programming to harness that computing power.
Answer: Anyone can be a Programmer (7 Votes) Consider how readily Alan Kay introduces children to programming by means of experiment and exploration in a programmable environment. People may study success in college-level courses and conclude "some people aren't fit to learn programming".
Proofs are programs.
Formal verification of programs is a huge research area. (See, for example, the group at Carnegie Mellon.)
Many complex programs have been verified; for example, see this kernel written in Haskell.
Programs absolutely can be proven to be correct. Lousy programs are hard to prove. To do it even reasonably well, you have to evolve the program and proof hand-in-hand.
You can't automate the proof because of the halting problem. You can, however, manually prove the post-conditions and preconditions of any arbitrary statement, or sequence of statements.
You must read Dijsktra's A Discipline of Programming.
Then, you must read Gries' The Science of Programming.
Then you'll know how to prove programs correct.
Just a small comment to those who brought up incompleteness -- it is not the case for all axiomatic systems, only sufficiently powerful ones.
In other words, Godel proved that an axiomatic system powerful enough to describe itself would necessarily be incomplete. This doesn't mean it would be useless however, and as others have linked to, various attempts at program proofs have been made.
The dual problem (writing programs to check proofs) is also very interesting.
You can in fact write provably correct programs. Microsoft, for example, has created an extension of the C# language called Spec# which includes an automated theorem prover. For java, there is ESC/java. I'm sure there are many more examples out there.
(edit: apparently spec# is no longer being developed, but the contract tools will become part of .NET 4.0)
I see some posters hand-waving about the halting problem or incompleteness theorems which supposedly prevent the automatic verification of programs. This is of course not true; these issues merely tell us that it is possible to write programs which cannot be proven to be correct or incorrect. That does not prevent us from constructing programs which are provably correct.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With