Module SuccSplits

Provides a predicate for the successor relation with split information, as well as logic used to construct the type TSplits representing sets of splits. Only sets of splits that can be reached are constructed, hence the predicates are mutually recursive.

For the successor relation

succSplits(ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits, Completion c)

the following invariants are maintained:

1. pred is reachable with split set predSplits.
2. For all split in predSplits:
   • If split.hasSuccessor(pred, succ, c) then split in succSplits.
3. For all split in predSplits:
   • If split.hasExit(pred, succ, c) and not split.hasEntry(pred, succ, c) then split not in succSplits.
4. For all split with kind not in predSplits:
   • If split.hasEntry(pred, succ, c) then split in succSplits.
5. For all split in succSplits:
   • split.hasSuccessor(pred, succ, c) and split in predSplits, or
   • split.hasEntry(pred, succ, c).

The algorithm divides into four cases:

1. The set of splits for the successor is the same as the set of splits for the predecessor: a) The successor is in the same SameSplitsBlock as the predecessor. b) The successor is not in the same SameSplitsBlock as the predecessor.
2. The set of splits for the successor is different from the set of splits for the predecessor: a) The set of splits for the successor is maybe non-empty. b) The set of splits for the successor is always empty.

Only case 2a may introduce new sets of splits, so only predicates from this case are used in the definition of TSplits.

The predicates in this module are named after the cases above.