Re: TEST categorize test suites

On March 13, Jeremy Carroll writes:
> 
> > ACTION Jeremy Carroll: look up different test suites and categorize
> 
> Summary:
> ========
> 
> Categories found:
> A: entailment
> B: class satisfiable
> C: consistency between class and instance of class.
> (Both postive and negative.)
> 
> B is a special case of C.
> 
> =================================
> 
> I have had a fairly brief look at Ian's [1] and Deb's (jtp) [2] test cases.
> 
> Most of the tests could be expressed as some class is or is not satisfiable.
> 
> The jtp cardinality tests were simple tests that systematically exercised a
> feature (cardinality).
> 
> Ian's tests covered a variety of objectives.
> Some appeared to be taken from published work, which looks like a *good
> thing*.
> 
> Some were performance tests, which appeared designed to stress test the
> software.
> I suggest such tests are not in scope for the test cases part of OWL.

I agree. Only a few of the tests are in this category however (mostly
ones relating to cardinality constraints with large numbers).

> Some important tests, which I think will help differentiate between
> implementation thoroughness were ones that required infinite models.
> I believe that Ian's approach depends on all counter-examples being finite,
> but clearly code that tries building the model to show satisfiability would
> have trouble.

The idea is that for some classes there are only infinite models. A
model building approach to proving satisfiability needs to be quite
sophisticated to deal with these cases - it needs to be able to
construct finite representations of infinite models (e.g., models with
loops in that represent infinite repetitions), and this makes
guaranteeing both termination and correctness rather tricky.

The examples include both cases where the prover would have to build
one of these "pseudo" models (i.e., all real models are infinite), and
cases that provide tricky termination conditions to exercise loop
checking code (i.e., where no model exists, but simple loop checking
can generate incorrect "models").

It would also be very interesting to see how other kinds of prover
deal with these kinds of test. I was hoping to see some of these tests
translated into DAML+OIL ontologies, which would have made it easy to
perform such testing. Is this going to happen?

Ian

> A few of the jtp tests did not seem to be to be easily transformable into
> satisfiable tests e.g. (forgive the lisp)
> 
> 
>         (max-cardinality child Person 4)
>         (min-cardinality child Person 1)
>         (Instance-of  fred  Person)
>         (max-cardinality child  fred  7)
>         (min-cardinality child  fred  6)
> 
> 
> which gives a contradiction, but not because there are unsatisfiable
> classes.
> 
> 
> So, in summary, I think we have seen example tests that are in scope and
> relevant of the following three forms:
> 
> - entailment (from Dan)
> - class satisfiable
> - consistency between class and instance of class.
> 
> Both postive and negative.
> 
> I note that class satisfiable can be expressed as the consistency between
> the class and a blank instance.
> 
> Other than that I do not believe that we should expect all tests of any one
> of these forms to be easily expressible in another one of these forms.
> (Given enough logical machinery I suspect such mappings are possible, but
> IMO test cases should attempt to assume only a small amount of machinery.)
> 
> 
> I am imagining that John will identify a much broader range of test types
> that will complement this list.
> 
> More examples of test suties would be welcome.
> 
> 
> Jeremy
> 
> [1] http://www.cs.man.ac.uk/~horrocks/Private/DAML/Tests/
> [2]
> http://ksl.stanford.edu/projects/DAML/chimaera-jtp-cardinality-test1.daml

Received on Friday, 5 April 2002 05:18:48 UTC