Verifying Chipmunk intervals (was: Level 2 query, number 2)
Let's start with the easy one: (Chipmunk Inc. is a John Pryce hypothetical)
> And could I run tests to check the following, which is IMO an important
> property of a representation?
> ss=w(xx) implies xx=r(ss),
> whence distinct internal intervals xx have distinct representations ss.
Monte Carlo methods are very powerful at checking verifiable things like this.
We expect there to be an interval equality test, and means to initialise
intervals to valid enclosures of two given floating-point values. By using
lots of random input intervals and checking each round-trip conversion we
should find out fairly quickly if recoverability fails. We would also use
a bunch of directed test cases to stress suspected edge conditions.
If Chipmunk Inc is really devious and intent on deceit, it could of course
have implemented undercover communication between the w(), r() and eq()
functions -- but by running separate instances of Chipmunk software, on
separate machines, with only text strings being exchanged among machines,
this type of cheat becomes difficult.
We can actually test more: we can check the tightness of Chipmunk's
enclosures. The documentation of the external format must be such that
each ss generated by w(xx) can be converted to a standard [lo,hi] pair
of any desired precision, so we can check the relationship between the
input and output of [inlo,inhi] -> xx -> ss -> [outlo,outhi] for a
number of cases. Writing the program that performs "ss -> [outlo,outhi]"
will expose any deficiencies in the required documentation of the ss format.
Once tightness bounds have been derived, we can generate distinct Chipmunk
intervals, and complete the verification.
If there is a large amount of non-determinacy (i.e. the same input leads
to different outputs on different occasions) these tests would be more
difficult, but Chipmunk's implementation would already earn a bad rep.
Michel.
---Sent: 2011-09-06 16:39:41 UTC