James Watson wrote > I you define correctness as passing all tests, creating a > new test that exposed an existing issue (with regard to > specifications) would make the code incorrect.
And why would we create a new test?
> > How are implementations normally checked against > > specs? ... > > Testing.
So normally tests represent the specification?
> How is this incompatible with what I am arguing?
The only way we can validate a program 'meets all requirements' is to ask someone "is this what you wanted?".
We can verify that a program is 'correct' by demonstrating that it satisfies the spec.
> > When we use tests to check the program conforms to > > spec, and the program passes all tests, and we're using > > an ordinary definition of program correctness, then the > > program is obviously 'correct'. > > If all tests pass, it doesn't mean that the spec is > completely satisfied unless the spec is defined by the > tests.
It isn't true unless it's true! What a tortuous way to avoiding saying - if the spec is defined by tests and all the tests pass then the spec is completely satisfied.
> In practical terms, it's possible to test a program and > have a good confidence in it's correctness. But you can > never prove a program to be correct in the terms that > Achilleas Margaritis describes as "proving correctness > means to mathematically prove that a piece of software > does what it should do." And this the commonly understood > defintion between myself and Achilleas when you decided to > start an argument about what correct means.
You can never mathematically prove a program to be correct when your idea of 'correct' is 'meets all requirements' - it's a category error - 'meets all requirements' is outside the formal domain of mathematics.
Previous Topic
