Recently for a software engineering exam, I had to answer an interesting Schach's problem from "Object-Oriented and Classical Software Engineering" 6th edition, McGraw Hill, 2005 (ISBN: 0-07-286551-2)
Can correctness proving solve the problem that the product as delivered to the client may not be what the client really needs? Give reasons for your answer.
Correctness proving aka program correctness aka correctness, can be formally defined as " formal mathematical demonstration that the semantics of a program is consistent with the specifications of that program". Fancy word for mathematical unit testing assertions? Not exactly but pretty close.
The author, Stephen Schach provides a strong argument against correctness proving being an absolute measure of client's satisfaction needs in the Naur Text processing problem. As he further elaborates on difficulties with correctness being a true measure.
- How do we find input–output specifications, loop invariants?
- What if the specifications are wrong?
- We can never be sure that specifications or a verification system are correct
As much as I agree with the practical accuracy of this statement, I believe in theory, program correctness can truly serve as an absolute measure of client's needs. It is true that current tool-sets at our disposal doesn't provide the level of sophistication but it's not NP-Complete. If we see how far SE's vision implemented with CS has brought us in the world of software testing, it seems to me not too far fetched prediction that with formal methods properly implemented and specs correctly written, system can be deterministic about WYSIWYG. Don't you think so? . Some references.
- An Introduction to Proving the Correctness of Programs
Sidney L. Hantler, James C. King
September 1976 ACM Computing Surveys (CSUR), Volume 8 Issue 3
- An Assessment of Techniques for Proving Program Correctness
June 1972 ACM Computing Surveys (CSUR), Volume 4 Issue 2
- Cleanroom software engineering for zero-defect software
Richard C. Linger
May 1993 Proceedings of the 15th international conference on Software Engineering
- NRL invitational workshop on testing and proving: two approaches to assurance Carl E. Landwehr, Susan L. Gerhart, John McLean, Donald I. Good, Nancy Leveson
1986 ACM SIGSOFT Software Engineering Notes, Volume 11 Issue 5
- An Assessment of Techniques for Proving Program Correctness
1972 ACM Computing Surveys (CSUR), Volume 4 Issue 2
- Quality, cleanroom and formal methods
Zarrin Langari, Anne Banks Pidduck May 2005
ACM SIGSOFT Software Engineering Notes , Proceedings of the third workshop on Software quality 3-WoSQ, Volume 30 Issue 4
ok, 'nuff about correctness, now some CFP's Non Sequitur
- MSR's International Symposium on Intelligent Environments (Improving the quality of life in a changing world)
- IPMU 2006, Session on Chance Discovery (Yukio Ohsawa)
- 2nd CFP: CPAIOR 2006: 3rd International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (ian miguel)
- CFP: BASeWEB @ AAMAS 2006 (Maria Fasli)
- Call for Participation: Intelligent User Interfaces 2006 (Tessa Lau)
and I have no idea why I'm writing this while watching batman begins, I mean seriously. Fight your fear Bruce!
