DPJizer makes the write effects of a foreach loop disjoint across different iterations of the loop by ensuring the the loop index variable appears in every write effect. For example, given a DPJ foreach loop with index variable j and a write effect e = writes Pi7[idx3 <- j], DPJizer has to come up with a set of values for region variables that make j appear in e. In this simple case, either Pi7 should contain the RPL element [j] directly or Pi7 should contain the RPL element [idx3] so that [j] appears in the effect after applying the substitution [idx3 <- j].
DPJizer makes the write effects of a foreach loop disjoint across different iterations of the loop by ensuring the the loop index variable appears in every write effect. For example, given a DPJ foreach loop with index variable
jand a write effecte = writes Pi7[idx3 <- j], DPJizer has to come up with a set of values for region variables that makejappear ine. In this simple case, eitherPi7should contain the RPL element[j]directly orPi7should contain the RPL element[idx3]so that[j]appears in the effect after applying the substitution[idx3 <- j].