defining "interoperability" (was Re: SML interop test plan)

On 17 Apr 2008, at 09:40 , Wilson, Kirk D wrote:

 > This is a good start on a difficult topic to think about.
 > Here’s a wild question I have on lines 37-38 (in section 5):

 >      For the purpose of this test plan, two implementations are
 >      said to be interoperable if they produce identical model
 >      validation result for each test case that tests a required
 >      feature of SML and SML-IF.

 > What is the primary object of interoperability?  Are
 > “implementations” said to be interoperable (only once implied
 > in the SML-IF spec), or are interchange models “interoperable”
 > (which seems the dominant view in the SML-IF spec, see section
 > 4.5), or is an SML-IF document “interoperable” (also in the
 > SML-IF spec, and SML-IF “document” is close enough to
 > “interchange model” to make this case essential equivalent to
 > the immediately preceding case).  Are we defining a new sense
 > of “implementation interoperability” for purposes of the test
 > plan?

In the course of yesterday's call, I took an action to send an
email to respond to Kirk's question with the proposal I made
orally during the meeting.

I propose (unless we find preferable alternative terminology,
which I am not proposing) that we overload the term
"interoperable" depending on the number and types of things we
are speaking about.

To make the intended usages clear, I am going to offer suggested
usages both in prose and in an ad-hoc version of formal logic;
the formalism should not be taken too seriously, it's mostly an
attempt to reduce ambiguity.

First, the basics.

(1) As a building block, I propose that we say that two
implementations interoperate with respect to a given model or
package (or equivalently that a model or package is interoperable
with respect to two given implementations) if and only if both
produce the same result when asked to check it: valid, conforming
but invalid, non-conforming (not a model).  In logical formalism:

   (forall I1, I2, M) (interop(I1, I2, M) iff
       implementation(I1)
       & implementation(I2)
       & model(M)
       & validationresult(I1,M) = validationresult(I2,M))

This appeals to several functions whose meanings are, I hope,
obvious: implementation(X) = 'X is an implementation', model(X) =
X is a model, validationresult(X,Y) = 'result of validating model
Y using implementation X'.  (I continue to worry about how
crisply we've defined the result of SML validation, but if we
assume it's defined or definable, then we just say that whatever
a result is, validationresult returns one.)

Now, using this building block we define the two usages Kirk
identified.

(2) A model (or an interchange package) is "interoperable" in an
absolute sense, without qualification, if and only if for any two
conforming implementations, the two implementations produce the
same result for the model.

   (forall M)(interoperable(M) iff
      model(M)
      & (forall I1, I2)
          (implementation(I1) & implementation(I2) -->
             validationresult(I1,M) = validationresult(I2,M)))

(3) Two implementations are interoperable without qualification
if and only if for any model, the two implementations produce the
same validation result.

   (forall I1, I2)(interoperable(I1, I2) iff
     implementation(I1)
     & implementation(I2)
     & (forall M)(model(M) -->
         validationresult(I1,M) = validationresult(I2,M)))

Some useful qualified forms of the term "interoperable" can also
be formulated.

(4) A model is interoperable with respect to some set of
implementations iff any two implementations in the set
interoperate with respect to that model.

   (forall M,S)(interoperable(M,S) iff
     model(M)
     & set(S)
     & (forall I)(I in S --> implementation(I))
     & (forall I1, I2)(I1 in S & I2 in S -->
         interop(I1,I2,M)))

The definition above has as a consequence that if M is
interoperable with respect to some set of implementations, all
implementations in the set get the same validation result for M.

(5) Two implementations are interoperable with respect to a
particular set of models if and only if they are interoperable
with respect to each model in the set.

   (forall I1, I2, S)(interoperable(I1, I2, S) iff
     implementation(I1)
     & implementation(I2)
     & set(S)
     & (forall M)(M in S --> model(M))
     & (forall M)(M in S -->
         validationresult(I1,M) = validationresult(I2,M)))

(6) And finally a set of implementations can be said to be
interoperable (or to interoperate) with respect to a set of
models if all the implementations in the implementation set get
the same validation result for each model in the model set.

   (forall Si, Sm)(interoperable(Si,Sm) iff
     set(Si),
     & set(Sm),
     & (forall I)(I in Si --> implementation(I))
     & (forall M)(M in Sm --> model(M))
     & (forall I1, I2, M)(
         I1 in Si
         & I2 in Si
         & M in Sm
         --> interop(I1,I2,M)))

There is a set of models, for example, that is interoperable with
respect to all conforming implementations.  There is a larger set
that is interoperable with respect to all conforming
implementations which support all optional features.  And so on.

I don't know how much of this, if any, we want to have in the
test plan.  But I think if we agree on this way of thinking about
things, we can at least understand each other when we talk
sometimes about models being interoperable, and sometimes about
implementations being interoperable.  Both are sensible things to
talk about.

--CMSMcQ

Received on Friday, 19 September 2008 19:31:35 UTC