
| op(X,Y)   |        |
|-----------|--------|
| Pre:      | p(X,Y) |
| q(X,Y)    |        |
| Ad:       |        |
| Del:      | p(X,Y) |

and an initial state in which p(a, c), p(b, c), g(b, d)
hold, the following two property spaces are constructed:

$p_{1}$, $q_{1}$$p_{1}$$q_{1}$$a$, $b$$p_{1}$, $q_{1}$, $p_{1}$, $q_{1}$, $q_{1}$$p_{2}$, $q_{2}$$q_{2}$$c$, $d$$q_{2}$, $p_{2}$$p_{2}$, $q_{2}$, $p_{2}$, $q_{2}$
Given these property spaces it is impossible to distinguish a from b or c from d, even though analysis of the operator schema and initial state reveal that a is functionally distinct from b and c from d. It can be seen that, although a must always exchange a pl for a ql, b can have both pl and ql simultaneously. A similar observation can be made for c and However, the process by which invariants are constructed cannot gain access to this d .

information. An identity invariant constructed for the first property space is:

$$x:T$$
$y$$z$$u$$(q\,(x,\,y)$$q\,(x,\,z)$$q\,(x,\,u)$$y=z$$y=u$$z=u)$.  
This invariant is weaker than is ideal, because acan participate in only one q relation (bcan participate in two simultaneously). A state membership invariant for this property space is:
x : T   ((  y : T 1   p(x, y))

$$p(x,\,y))$$

y : T 1 g ( x, y ))
which understates the case for b, which can have p 1 and q 1 simultaneously.  No unique state invariant is constructed for this property space, because p 1 and q 1 are not mutually exclusive.

## 3.1  Correct Ness And Completeness Of The Transition Rule Construction Phase

The correctness of the algonthm used in TIM depends on two elements. Firstly, the property spaces identified by the algorithm must be correctly populated. That is, no objects should be assigned to property spaces to which they do not belong and every achievable state must be included in the appropriate property space. Secondly, these property spaces must only support the generation of correct invariants. This second element is examined in Section 3.2.

An interesting relationship exists between the states in a property space and the invariants generated from the space. Incorrect invariants will be contructed if a property space is missing achievable states. This is because the state membership invariants assert that each object in the property space must be in one of the states in the property space. If states are missing then this invariant will be false. We now prove that all achievable states will be in the appropriate property space.

Theorem 1 Given an initial state, I, a collection of operator schemas, O, a property space, P = (Ps,TRs, Ss, Os), generated by TIM when applied to I and O, and any state, St, which