In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value of x which satisfies it. Similarly it is possible to specify objects using the formal specification language Z 3,4], which can not possibly exist. Such specifications are called inconsistent and can arise in a number of ways. Example 1 The following Z specification of a functionf, from integers to integers "f x: 1 x O. fx = x + 1 (i) "f x: 1 x O. fx = x + 2 (ii) is inconsistent,...