Re: Float conversion

[Phil Clayton <phil.clayton@lineone.net>]

On Aug 4, 8:26 am, Stephen Leake <stephen_le...@stephe-leake.org>
wrote:
> >> > Where does the original justification go wrong?  Well, when talking
> >> > about 'the smallest' there is an implicit assumption being made that
> >> > it is unique.  The justification never considers the case when A or B
> >> > is the non-unique smallest.
>
> >> And the same error could be made in a formal specification. "formal"
> >> does _not_ mean "complete"!
>
> > Although I said "formal methods", I use this example to motivate
> > formal verification, not formal specification.  Any specification,
> > formal or not, can be a load of rubbish!
>
> What are you verifying, if not a specification?
>
> If the specification is rubbish, what is the point of verifying it?

Well, in practice, you would hope that if someone knew a specification
was wrong/incomplete that they wouldn't go ahead and implement it!

What if a specification is clear but - not obviously - contains
undesired features?  It can be argued that a convincing verification
is valuable regardless of the specification quality because, when
something goes wrong, you know that it is less likely to be an
implementation issue and more likely to be a specification issue.  So
it helps isolate issues.  In practice, any sane person would review
the specification first to reduce the likelihood of change and
subsequent process iteration.

So there are two separate issue here:
1. Is the specification capturing what is wanted (`validation')
2. Does the program implement the specification (`verification')

I was only considering 2 in this thread and trying to avoid the other
minefield that is 1!

Phil