For loops can be analyzed to determine their data dependencies and apply transformations to assist in their parallelization.  The commands support array indices that are polynomials with rational coefficients.  Here is an example of how a nested for loop can be transformed so that the inner loop can be parallelized:

The following procedure has dependencies across both the $i$ and the $j$ loop indices and cannot be easily parallelized in this form:

$$\begin{gathered} p ≔ \mathbf{proc}\left(A\right) \\ \mathbf{local} i\, j\: \\ \mathbf{for} i \mathbf{from} 1 \mathbf{to} 3 \mathbf{do} \\ \mathbf{for} j \mathbf{from} 1 \mathbf{to} 3 \mathbf{do} \\ A\left[i\,j\right] ≔ A\left[i - 1\, j\right] \+ A\left[i\, j - 1\right]\: \\ \mathbf{end} \mathbf{do}\: \\ \mathbf{end} \mathbf{do}\: \\ \mathbf{end} \mathbf{proc}\: \end{gathered}$$

$\mathrm{loop} ≔ \mathrm{CreateLoop}\left(p\right)\:$

The dependencies in this loop cross both the $i$ and $j$ dimension, as can be seen in the equation of its dependence cone:

$\mathrm{DependenceCone}\left(\mathrm{loop}\, A\, \left[\mathrm{di}\, \mathrm{dj}\right]\right)\;$

Applying a transformation to the loop will change the relationship between the data dependencies:

$\mathrm{transformation\_matrix} ≔ ⟨⟨1 \| 1⟩\, ⟨0\|1⟩⟩\;$

$\mathrm{transformed\_loop} ≔ \mathrm{UnimodularTransformation}\left(\mathrm{loop}\,\mathrm{transformation\_matrix}\right)\:$

$\mathrm{GenerateProcedure}\left(\mathrm{transformed\_loop}\right)\;$

This transformed loop no longer has a relationship between the dimensions its distance vectors:

$\mathrm{DependenceCone}\left(\mathrm{transformed\_loop}\, A\, \left[\mathrm{dn}\,\mathit{ }\mathrm{dm}\right]\right)\;$

The data dependencies in the loop body only depend on previously computed elements.  The pattern for updating the array in the original and transformed loops are shown below.  The inner loop of the transformed program corresponds to the anti-diagonal lines of the array updates.  These updated operations can be performed simultaneously since they only refer to previously updated array entries (those entries that point toward a particular array entry).

The set of array indices for all values of the loop's index variables can also be computed:

$\mathrm{ispace} ≔\mathrm{IterationSpace}\left(\mathrm{loop}\right)\;$

$\mathrm{isolve}\left(\mathrm{convert}\left(\mathrm{ispace}\,\mathrm{set}\right)\right)\;$

The while loop related commands can be used to formally verify that a procedure meets its specification.  The invariants of a while loop can be computed and, when combined with the pre-condition and guard condition of the loop, used to verify whether or not the post-condition will be satisfied.  This verification indicates whether or not the $\mathrm{ASSERT}$ statement after the loop will always be true.  Loops whose assignments are polynomials with rational coefficients are supported.

The following example shows how the invariants of a while loop can be computed and used to verify that the following program is free from errors and meets its specification encoded in the last $\mathrm{ASSERT}$ statement of the procedure:

$$\begin{gathered} \mathrm{z3sqrt} ≔ \mathbf{proc} \left(a\&comma; \mathrm{err}\right) \\ \mathbf{local} r\&comma; q\&comma; p\&semi; \\ r ≔ a - 1\&semi; \\ q ≔ 1\&semi; \\ p ≔ 1\&sol;2\&semi; \\ \mathrm{ASSERT}\left(a \le 4 \mathbf{and} 1 \le a \mathbf{and} 0 < \mathrm{err} \mathbf{and} p \&gt; 0 \mathbf{and} r \ge 0 \right)\&semi; \\ \mathbf{while} \mathrm{err} \le 2 \&ast; p \&ast; r \mathbf{do} \\ \mathbf{if} 0 \le 2 \&ast; r - 2 \&ast; q - p \mathbf{then} \\ r ≔ 2 \&ast; r - 2 \&ast; q - p\&semi; \\ q ≔ q \&plus; p\&semi; \\ p ≔ 1\&sol;2 \&ast; p\&colon; \\ \mathbf{else} \\ r ≔ 2 \&ast; r\&semi; \\ p ≔ 1\&sol;2 \&ast; p\&colon; \\ \mathbf{end} \mathbf{if}\&colon; \\ \mathbf{end} \mathbf{do}\&semi; \\ \mathrm{ASSERT}\left(q\&Hat;2 \le a \mathbf{and} a < q\&Hat;2\&plus;\mathrm{err}\right)\&semi; \\ \mathbf{return} q\&colon; \\ \mathbf{end} \mathbf{proc}\&colon; \end{gathered}$$

Create the WhileLoop data structure:

$\mathrm{loop} ≔ \mathrm{CreateLoop}\left(\mathrm{z3sqrt}\right)\&colon;$

In this case, a loop invariant needs to be computed to formally verify the loop:

$\mathrm{invariant} ≔ \mathrm{LoopInvariant}\left(\mathrm{loop}\&comma; \mathrm{invarianttype} \&equals; \mathrm{absolute}\right)\&semi;$

The return value of $\mathrm{true}$ indicates that the procedure is guaranteed to meet its specification:

$\mathrm{VerifyLoop}\left(\mathrm{loop}\&comma; \mathrm{invariant}\right)\&semi;$