Darren New <dne### [at] sanrrcom> wrote:
> Nicolas Alvarez wrote:
> > Darren New wrote:
> >> Warp wrote:
> >>> Orchid XP v8 <voi### [at] devnull> wrote:
> >>>> Eiffel has preconditions *and* postconditions, which most people don't
> >>>> seem to bother checking with assert() calls.
> >>>   A little thought experiment: How would you write a comprehensive
> >>> postcondition to a function that sorts a list/array of elements?
> >> Trivial.
> >>
> >> Forall(i < length-1) assert(j[i]<=j[i+1]);
> >>
> >> Basically, the definition of sorting. Of course, you need to be able to
> >> put qualifiers in your assertions.}
> > 
> > A sorting function that, given any input, returns [1,2,3,4,5], will pass 
> > that test.

> Heck, for that matter anything returning a zero-length array would pass. OK, 
> to be *comprehensive*, you would have to add that the result is a 
> permutation of the original. You could do this by counting how many times 
> each original value occurs in the list and making sure it occurs in the 
> result the same number of times.

  That was one warning example at school aboit how easy it is to write
pre- and postconditions which actually are not comprehensive enough.
The sorting example is superb to demonstrate that, because many people,
like you, think that it's enough to go through the array after the sorting
is done and check that every value is larger or equal to the previous value.
The counter-example to this is, of course, to make the "sorting" fill the
array with the same value (eg. the first one), and it would pass the test.

  At the same time it poses an interesting thought problem: *How* would you
write a post-condition that truly checks that the resulting array has the
same values as the original, but sorted? And a bit more difficult: What
would be the asymptotically fastest possible way of doing the check?

-- 
                                                          - Warp

Post a reply to this message