> 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?
Why wouldn't we? Is there an argument here?
> > > > 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?".
No, it's not.
> We can verify that a program is 'correct' by demonstrating > that it satisfies the spec.
The spec is derived from the requirements. It's documentation of the requirements. Validating against the spec is validating against requirements as long as the specifications accurately represent the requirements. This is the point of documenting the requirements in the specification and getting people to agree that they represent the requirements. Once this is completed, the specifications are considered to be the requirements.
> > > 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.
I'm not avoiding saying that. It's a tautology. There's no need to point it out. If the floor is 'what I stand on' then 'what I stand on' is the floor. You can prove any statement if you can choose your axioms. Logic is only relevant to the 'real' world if we choose axioms that match our experience.
Almost no real specifications are documented in this way and most applications requirements that can be specified in other manners cannot be specified with tests. When did everyone in this thread agree that we were only talking about this minuscule subset of specifications?
> 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.
Nonsense. Specifications are the formal statement of requirements. From a development perspective, the specifications are the requirements.
Let's say hypothetically that I agree that "meets all requirements" is not the proper way to state what I meant and I should have said "valid with respect to it specifications". It really makes no difference because for all intents and purposes, these are basically equivalent statements. But let's say I agree that I was wrong to state it that way. What would that prove exactly?
I'll even agree to use the term specification from now on at least in the context of this thread. Will that satisfy you?