Warp wrote:
>   That was one warning example at school aboit how easy it is to write
> pre- and postconditions which actually are not comprehensive enough.

Yes, it's a good point. :-)

> 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.

Obviously had it not been an offhand post to p.o-t I would have put more 
thought into it. I thought you were asking more about the technology of how 
it was done, and I was saying "obviously you need universal qualifiers like 
this..." rather than trying to actually be comprehensive.

>   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? 

Sure. As I said, you can loop thru the original array, counting the number 
of times old[i] appears in old, then for each of those loop thru new[j] 
counting the number of times old[i]==new[j].  So it's at worst O(N^2).

It's not hard to specify, which is what I thought you were getting at. Hard 
to do efficiently, but that's what people do in debug builds.

For example, MS has a rule that you're not allowed to publish performance 
reviews of their beta software. At one point, they gave a beta of Excel to a 
journalist, and they tried it out, and published that it was terribly slow. 
Well, it was a debug build, and every time you did an update, it would 
calculate everything with the optimized path, then it would iteratively 
calculate every single cell over and over until it stabilized (or they 
looped more than the number of cells), and then compared the two. Of course 
it was slow.

Once you're confident your sort works, you don't have to test you haven't 
introduced new values in production. :-)

-- 
Darren New, San Diego CA, USA (PST)
    Eiffel - The language that lets you specify exactly
    that the code does what you think it does, even if
    it doesn't do what you wanted.

Post a reply to this message