Languages, 1986.

11 Implementation All transformations in this paper can be automated, but testing the mutual exclusion of run-time rules is not even decidable: Let w � v be inputs to the Turing Machine M and be an evolving algebra simulating simultaneously the computations of M on w and on v. Assume that halt(x) is set to true, as soon as the simulation of M on x halts and that the rules of contain the following rules: if halt(w) then u1 if halt(v) then u2 Since it is undecidable to test, whether M holds on an input, it is undecidable, whether halt(w) andhalt(v) could not be true at the same time. Nevertheless heuristics can be used to decide, whether the conditions are mutually exclusive. But in general some conditions, whicharemutually exclusive, can not be detected. Even checking mutual exclusion at run-time is co-NPcomplete ([Gur91])