Registered: Jul, 2003
Re: word games
Posted: Aug 4, 2007 7:41 PM
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?
I don't suppose we're creating new tests just for the fun of it, so there must be some other motive, such as - the existing tests don't adequately represent the spec, the spec changed...
> > The only way we can validate a program 'meets all
> > requirements' is to ask someone "is this what you
> > wanted?".
> No, it's not.
Yes it is.
> > We can verify that a program is 'correct' by
> > 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
> e specification and getting people to agree that they
> represent the requirements. Once this is completed, the
> specifications are considered to be the requirements.
Yes, the spec is derived from requirements.
No, the spec is not considered to be the requirements - see exception clause "as long as the specifications accurately represent the requirements".
> 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.
Your omniscience with respect to how real specifications are documented leaves nothing for me to say.
> > You can never mathematically prove a program to be
> > 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.
Sense. From a development perspective, specs are a formalization of the requirements - thinking they are the requirements is a sign of confusion.
> 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
If you're talking about conforms to spec and Achilleas Margaritis is talking about conforms to spec, then we should wonder what he meant when he wrote "I would like to point out that proving statically that software is correct is impossible." [Jul 30, 2007 6:51 AM]
Maybe he was talking about the halting problem?
Maybe he meant impractical rather than impossible?
Maybe (given that he followed with "A static type system only proves that what you typed makes some kind of sense") he was only talking about what the "static type systems of C/C++/Java/C#" [Aug 2, 2007 10:17 AM] can do, not what other tools can do?
If Achilleas wasn't invoking the halting problem, and wasn't restricting his comments to compiler type systems, and really meant impossible rather than impractical - is he right?