Create Loop - Maple Help

CodeTools[ProgramAnalysis]

 CreateLoop
 create a WhileLoop or ForLoop from a Maple procedure

 Calling Sequence CreateLoop(p)

Parameters

 p - procedure with a loop

Description

 • This command processes the procedure p and returns either a ForLoop or a WhileLoop data structure, depending on p's form.  Both for loops and while loops are represented in Maple using do statements.  In this package, a for loop is understood to be a loop that iterates over some index variable(s), reading from and updating the entries of an indexable variable, i.e. an Array, Matrix, Vector or table.  A while loop is a loop that recursively updates its loop variable(s) until its guard condition (while clause) is no longer satisfied.

For Loops

 • The procedures that can be converted to ForLoops have a particular structure.  They consist of initialization statements, followed by a (possibly nested) for loop.  More precisely, they can be defined as follows, where $\mathbf{::=}$ means "defined as", $|$ means "or", and ${\left\{\dots \right\}}^{+}$ means one or more of the enclosed:
 $\begin{array}{cc}& \mathrm{ForLoopProcedure}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{::=}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{proc}\left({p}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{p}_{m}\right)\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathbf{local}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{v}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{v}_{n}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{x}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{x}_{p}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}};\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{# Initialization statements}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}{x}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔{f}_{1}\left(p\right);\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}{x}_{2}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔{f}_{2}\left(p,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{x}_{1}\right);\hfill \\ & \phantom{\rule[-0.0ex]{4.5ex}{0.0ex}}⋮\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}{x}_{p}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔{f}_{p}\left(p,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{x}_{1},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{x}_{p-1}\right);\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{ForLoop}\hfill \\ & \mathbf{end proc}\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \end{array}$
 $\begin{array}{cc}& \mathrm{ForLoop}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{::=}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{for}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{v}_{i}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{from}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{\mathrm{lb}}_{i}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{to}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{\mathrm{ub}}_{i}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{LoopBody}\hfill \\ & \mathbf{end do}\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \end{array}$
 $\begin{array}{cc}& \mathrm{LoopBody}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{::=}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathrm{ForLoop}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}|\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathrm{IfStatement}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}|\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathrm{AssignmentStatements}\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \end{array}$
 $\begin{array}{cc}& \mathrm{IfStatement}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{::=}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{if}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{c}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{then}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{AssignmentStatements}\hfill \\ & \mathbf{elif}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{c}_{2}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{then}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{AssignmentStatements}\hfill \\ & \phantom{\rule[-0.0ex]{4.5ex}{0.0ex}}⋮\hfill \\ & \mathbf{else}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{AssignmentStatements}\hfill \\ & \mathbf{end if}\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \end{array}$
 $\begin{array}{cc}& \mathrm{AssignmentStatements}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{::=}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{\left\{{p}_{j}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{g}_{j}\left(p,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}v,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}x\right)\right\}}^{+}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \end{array}$
 • In addition, the loop must have the following properties:
 – The assignments in the loop body must assign to indexable variables
 – The indices of the loop's arrays must be polynomials with rational coefficients
 – The loops' lower bounds ${\mathrm{lb}}_{i}$ / upper bounds ${\mathrm{ub}}_{i}$ must be linear in the loops' index variables $v$, parameters $p$ and local variables $x$, or the max/min of a sequence of such expressions, respectively.  Optionally, the lower/upper bounds may have the ceil/floor function applied, respectively.
 • This command processes such procedures and returns a ForLoop data structure.  This data structure is a Record with the following fields:
 – $\mathrm{variables}$ : list of the loop's index variables, one per layer of nested for loops
 – $\mathrm{arrays}$ : list of indexable variables being read from or written to in the loop
 – $\mathrm{parameters}$ : list of the parameters passed to the procedure p that are not in $\mathrm{arrays}$
 – $\mathrm{initialization}$ : list of equations representing the assignments that occur before the loop
 – $\mathrm{layers}$ : listlist, one for each layer of for loop in p.  Each inner list consists of four elements: the loop variable name, the lower bound, the step size and the upper bound.
 – $\mathrm{body}$ : listlist, one entry for each if branch in the loop's body.  The inner lists have two elements: the conditional expression for the branch of the if statement and a list of equations representing the branch's statement sequence.

While Loops

 • WhileLoops can be generated from procedures that have the following form:
 $\begin{array}{cc}& \mathrm{WhileLoopProcedure}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{::=}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{proc}\left({x}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{x}_{m}\right)\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathbf{local}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{v}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{v}_{n}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{y}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{y}_{p}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}};\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{# Initialization statements}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}{y}_{1}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔{f}_{1}\left(x\right);\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}{y}_{2}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔{f}_{2}\left(x,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{y}_{1}\right);\hfill \\ & \phantom{\rule[-0.0ex]{4.5ex}{0.0ex}}⋮\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}{y}_{p}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}≔{f}_{p}\left(x,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{y}_{1},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\dots \phantom{\rule[-0.0ex]{0.5ex}{0.0ex}},\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}{y}_{p-1}\right);\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{ASSERT}\left(\mathrm{pre­condition}\right);\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathbf{while}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathrm{guard}­\mathrm{condition}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathbf{do}\hfill \\ & \phantom{\rule[-0.0ex]{4.0ex}{0.0ex}}\mathbf{if}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathrm{branch}­{\mathrm{condition}}_{1}\mathbf{then}\hfill \\ & \phantom{\rule[-0.0ex]{6.0ex}{0.0ex}}{v}_{1}≔{g}_{1}\left(v,x,y\right);\hfill \\ & \phantom{\rule[-0.0ex]{6.0ex}{0.0ex}}\cdots \hfill \\ & \phantom{\rule[-0.0ex]{6.0ex}{0.0ex}}{v}_{n}≔{g}_{n}\left(v,x,y\right);\hfill \\ & \phantom{\rule[-0.0ex]{4.0ex}{0.0ex}}\mathbf{elif}\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\mathrm{branch}­{\mathrm{condition}}_{2}\mathbf{then}\hfill \\ & \phantom{\rule[-0.0ex]{6.0ex}{0.0ex}}\cdots \hfill \\ & \phantom{\rule[-0.0ex]{4.0ex}{0.0ex}}\mathbf{else}\hfill \\ & \phantom{\rule[-0.0ex]{6.0ex}{0.0ex}}\cdots \hfill \\ & \phantom{\rule[-0.0ex]{4.0ex}{0.0ex}}\mathbf{end if};\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathbf{end do};\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathrm{ASSERT}\left(\mathrm{post­condition}\right);\hfill \\ & \phantom{\rule[-0.0ex]{2.5ex}{0.0ex}}\hfill \\ & \phantom{\rule[-0.0ex]{2.0ex}{0.0ex}}\mathbf{return}h\left(x,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}v,\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}y\right);\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}\hfill \\ & \mathbf{end proc}\hfill \end{array}$
 • In addition, the procedure must satisfy the following:
 – The WhileLoop cannot have any statements between the ASSERT statement for the pre-conditions and the do statement of the loop, or between the loop statement and the ASSERT statement for the post-conditions
 – The pre-conditions, post-conditions, branch conditions, and assignments to the loop variables $v$ must be polynomials with rational coefficients
 • A WhileLoop with only assignments inside the loop is equivalent to a loop with an if statement that only has an else clause.
 • The returned WhileLoop data structure has the following fields:
 – $\mathrm{variables}$ : list of the loop variables, i.e. variables updated in the loop.
 – $\mathrm{parameters}$ : list of the procedure's parameters.
 – $\mathrm{initialization}$ : list of initial values for the loop variables written in terms of the $\mathrm{parameters}$.
 – $\mathrm{precondition}$ : conditional expression extracted from the ASSERT statements before the loop.  These conditions are assumed to be true.
 – $\mathrm{guard}$ : conditional expression in the while clause of the do loop.
 – $\mathrm{transitions}$ : listlist, one entry for each if branch in the loop's body.  The inner lists have two elements: the conditional expression for the branch of the if statement and a list of values representing that branch's loop variable assignments.  These are the updated values that the loop variables will receive on the next iteration.  The loop variables may have been updated with sequential assignments in the original loop, but here they have been converted to one simultaneous assignment that is equivalent to a multiple assignment in Maple.
 – $\mathrm{postcondition}$ : conditional expression extracted from the ASSERT statements after the loop that may or may not hold after the loop's completion.  The VerifyLoop is used to determine whether or not the $\mathrm{postcondition}$ will be satisfied.
 – $\mathrm{returnvalue}$ : list of the procedure's return value(s).  The procedure's return value are the operands of $\mathrm{returnvalue}$.
 • The conditional expressions in the WhileLoop data structure represent boolean by using a list of elements to signify their disjunction and a set of elements to indicate their union.

Examples

 > $\mathrm{with}\left(\mathrm{CodeTools}\left[\mathrm{ProgramAnalysis}\right]\right):$

For Loop Example

 • We now set up a test procedure including a perfectly nested for loop.
 > for_proc := proc(a, b, n)     local i, j;     for i from 1 to min(n + 2, 10) do         for j from i to n + 2 do             a[i, j] := b[i + 1] + a[i - 1, j - 1]         end do     end do end proc:
 • Create the for loop data structure from the test procedure
 > $\mathrm{loop1}≔\mathrm{CreateLoop}\left(\mathrm{for_proc}\right):$
 • View the raw content of the data structure:
 > $\mathrm{op}\left(\mathrm{loop1}\right)$
 ${\mathrm{Record}}{}\left({\mathrm{ForLoop}}{,}{\mathrm{body}}{=}\left[\left[\left[\right]{,}\left[{{a}}_{{i}{,}{j}}{=}{{b}}_{{i}{+}{1}}{+}{{a}}_{{i}{-}{1}{,}{j}{-}{1}}\right]\right]\right]{,}{\mathrm{layers}}{=}\left[\left[{i}{,}{1}{,}{1}{,}{\mathrm{min}}{}\left({n}{+}{2}{,}{10}\right)\right]{,}\left[{j}{,}{i}{,}{1}{,}{n}{+}{2}\right]\right]{,}{\mathrm{initialization}}{=}\left[\right]{,}{\mathrm{variables}}{=}\left[{i}{,}{j}\right]{,}{\mathrm{parameters}}{=}\left[{n}\right]{,}{\mathrm{arrays}}{=}\left[{a}{,}{b}\right]\right)$ (1)
 • Convert the ForLoop back into a Maple procedure.
 > $\mathrm{GenerateProcedure}\left(\mathrm{loop1}\right)$
 ${\mathbf{proc}}\left({a}{,}{b}{,}{n}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{local}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{i}{,}{j}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{for}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{i}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{to}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{min}}{}\left({10}{,}{n}{+}{2}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{for}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{j}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{from}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{i}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{to}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{n}{+}{2}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{a}{[}{i}{,}{j}{]}{≔}{b}{[}{i}{+}{1}{]}{+}{a}{[}{i}{-}{1}{,}{j}{-}{1}{]}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end do}}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{return}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$ (2)

While Loop Example

 • Create a basic While Loop with pre- and post-conditions:
 > while_proc := proc (a, err)     local r, q, p;     r := a - 1;     q := 1;     p := 1/2;     ASSERT(a <= 4 and 1 <= a and 0 < err and p > 0);     while err <= 2 * p * r do         if 0 <= 2 * r - 2 * q - p then             r := 2 * r - 2 * q - p;             q := q + p;             p := 1/2 * p:         else             r := 2 * r;             p := 1/2 * p:         end if:     end do;     ASSERT(q^2 <= a and a < q^2+err);     return q: end proc; loop2 := CreateLoop(while_proc);
 ${\mathrm{while_proc}}{≔}{\mathbf{proc}}\left({a}{,}{\mathrm{err}}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{local}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{,}{q}{,}{p}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{a}{-}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{q}{≔}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{p}{≔}{1}{/}{2}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{ASSERT}}{}\left({a}{<=}{4}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{1}{<=}{a}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{0}{<}{\mathrm{err}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{0}{<}{p}\right){;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{while}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{err}}{<=}{2}{*}{p}{*}{r}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{if}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{0}{<=}{2}{*}{r}{-}{2}{*}{q}{-}{p}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{then}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{2}{*}{r}{-}{2}{*}{q}{-}{p}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{q}{≔}{q}{+}{p}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{p}{≔}{1}{/}{2}{*}{p}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{else}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{2}{*}{r}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{p}{≔}{1}{/}{2}{*}{p}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end if}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end do}}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{ASSERT}}{}\left({q}{^}{2}{<=}{a}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{a}{<}{q}{^}{2}{+}{\mathrm{err}}\right){;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{return}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{q}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$
 ${\mathrm{loop2}}{≔}{\mathrm{Record}}{}\left({\mathrm{WhileLoop}}{,}{\mathrm{variables}}{=}\left[{p}{,}{q}{,}{r}\right]{,}{\mathrm{parameters}}{=}\left[{a}{,}{\mathrm{err}}\right]{,}{\mathrm{initialization}}{=}\left[\frac{{1}}{{2}}{,}{1}{,}{a}{-}{1}\right]{,}{\mathrm{transitions}}{=}\left[\left[{0}{\le }{2}{}{r}{-}{2}{}{q}{-}{p}{,}\left[\frac{{p}}{{2}}{,}{q}{+}{p}{,}{2}{}{r}{-}{2}{}{q}{-}{p}\right]\right]{,}\left[\left[\right]{,}\left[\frac{{p}}{{2}}{,}{q}{,}{2}{}{r}\right]\right]\right]{,}{\mathrm{guard}}{=}\left({\mathrm{err}}{\le }{2}{}{p}{}{r}\right){,}{\mathrm{precondition}}{=}\left[\left[\left[\left[{a}{\le }{4}{,}{1}{\le }{a}\right]{,}{0}{<}{\mathrm{err}}\right]{,}{0}{<}{p}\right]\right]{,}{\mathrm{postcondition}}{=}\left[\left[{{q}}^{{2}}{\le }{a}{,}{a}{<}{{q}}^{{2}}{+}{\mathrm{err}}\right]\right]{,}{\mathrm{returnvalue}}{=}\left[{q}\right]\right)$ (3)

While Loops and Assignments

 • This WhileLoop uses sequential assignments:
 > while_proc_sequential := proc(a, b)     local i, j:     i := 1:     j := 1:     while a < b*j do         i := i + 1:         j := a*i + b:     end do:     return j: end proc: loop1 := CreateLoop(while_proc_sequential):
 • When converting back into a procedure using GenerateProcedure, however, the sequential assignments are converted into equivalent simultaneous assignments.  While the bodies of the loops in while_proc_sequential and while_proc_simultaneous are different, they are equivalent.
 > $\mathrm{while_proc_simultaneous}≔\mathrm{GenerateProcedure}\left(\mathrm{loop1}\right)$
 ${\mathrm{while_proc_simultaneous}}{≔}{\mathbf{proc}}\left({a}{,}{b}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{local}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{i}{,}{j}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{i}{,}{j}{≔}{1}{,}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{while}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{a}{<}{b}{*}{j}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{i}{,}{j}{≔}\left[{i}{+}{1}{,}{a}{*}\left({i}{+}{1}\right){+}{b}\right]\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end do}}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{return}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{j}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$ (4)

Compatibility

 • The CodeTools[ProgramAnalysis][CreateLoop] command was introduced in Maple 2016.