Well-definedness errors can occur in B in the following circumstances:
To ensure that your models only contain well-defined formulas, Rodin creates well-definedness proof obligations for Event-B and Atelier-B can create them for classical B. ProB will check for well-definedness during constraint solving, animation and model checking. However, by default this check is not very extensive. You can force ProB to look more aggressively for well-definedness issues in your formulas by setting the following preference to true:
However, even with this, the search is not guaranteed to be exhaustive. Also, ProB's constraint solving does not necessarily solve formulas from left to right. Hence, the following formulas will be considered well-defined (and on can argue that they are) by ProB:
Technically speaking, for disjunctions and implications ProB uses the L-system of well-definedness (i.e., for P => Q, P should be well-defined and if P is true then Q should also be well-defined).