Correctness Proving Rants - Call for Papers - etcetera etcetera

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.

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!