Re: Level 2 query, number 2
Michel, P1788
On 5 Sep 2011, at 14:03, Michel Hack wrote:
> (1) Export to a convenient and well-understood generic format...
>
> (2) Export exactly, documenting the format, or letting us define ...
>
> Neither method requires exposing proprietary details of the internal encoding.
> It is the external format that must be documented unambiguously.
>
> Both forms can indeed be seen as a contract...
I have some questions about the "strength" of contract that the standard should demand. Suppose we have an interval type provided by Chipmunk Intervals Inc.
I propose
PRINCIPLE.
The "contract" should give enough information for a user to perform
an independent audit of the Chipmunk type and its operations.
By audit I mean not a formal proof, but a battery of tests that give confidence (or not) in the correctness and tightness of enclosures produced by computing with this type.
Let xx denote an internal interval of Chipmunk type and ss its string representation. We have a "write" function w that converts xx to ss and a "read" function r that converts back.
(In motion 19 I think I used "s" instead of "w".)
w and r are pieces of computer code provided by Chipmunk Inc.
There is also a "value" function v that a human with paper and pencil can apply, to convert ss to a mathematical interval written on paper. (A computer is permitted to do this too.) v is defined by Chipmunk Inc's documentation, in a human-understandable way.
Q: Does that give enough information to audit the Chipmunk type?
My answer: I'm not sure, but I don't think so. If I were "auditing", I would want to run some interval calculations using an ordinary type, and a Chipmunk type, and compare the results. I think what's missing is a way to *create* input data that are exact Chipmunk intervals. Of course, P1788's I/O lets us read an interval in some string form, say "[0.1,0.2]", and convert it to a Chipmunk interval xx. Then xx must *enclose* [0.1,0.2], and we can get some conclusions from that. But it seems a crude approach.
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.
Seeking your opinions.
John Pryce