# Re: The Ugly Test

• From: Jeremy Carroll <jjc@hpl.hp.com>
• Date: Wed, 29 Jan 2003 08:17:33 +0100
• Message-Id: <200301290817.33320.jjc@hpl.hp.com>
```> after a exhausting day I hoped to find some compensation

Proving tests is light relief?

> (the range of p is a
> class with one element and i is in a restriction on property
> p with mincardinality of 1) so can someone give a hint?

Try exhaustive search ...

if S is a set with small cardinality then

x memberOf S
can be rewritten as
x = s1 or x = w2 or ... or x = sn

The hard bit - a test I've yet to write - is when the cardinality of S is not
so small e.g. 30, but some of the members fit one pattern, some of the
members fit a second, and the rest a third.

By hand you prove it
define S1 = first pattern
define S2 = second pattern
define S3 = third pattern
S = S1 union S2 union S3

x member of S
rewrites as
x member of S1 or x member of S2 or x member of S3

But ... if you have the exhaustive rule above, you can easily find yourself
exploring 30 possibilities where almost all the work is essentially the same
(where by hand one would say 'similarly' and be done with it).

Jeremy
```

Received on Wednesday, 29 January 2003 02:24:17 UTC