The main steps of our approach are as follows. (i) Let \(p(x)\)  be a polynomial
over variables \(x\)  and let \({s\ge 0}\)  be an upper bound on the number of
program variables to be used in the loop. If not specified, \(s\)  is considered to
be the number of variables from \(x\) .
(ii) We use syntactic constraints over the loop body to be synthesized and
define a loop template, as given by our programming
model (REF ). Our programming model
imposes that
the functional behavior of the synthesized loops can
be modeled by a system of C-finite recurrences (Section ).
(iii) By using the invariant property of \(p(x)=0\)  for the loops to the
synthesized, we construct a polynomial
constraint problem (PCP) characterizing the set of all
loops satisfying the constraints of (REF ) for which \({p(x) = 0}\) 
is a loop invariant (Section ). Our approach combines symbolic computation techniques over algebraic recurrence equations
with polynomial constraint solving. We prove that our approach to loop synthesis
is both sound and complete. By completeness we mean that if
there is a loop \(\mathcal {L}\)  with at most \(s\)  variables satisfying the
invariant \({p(x)=0}\)  such that the loop body meets our C-finite/affine syntactic
requirements, then \(\mathcal {L}\)  is synthesized by our method (Theorem REF ).
Moving beyond \(s\) , that is, deriving an upper bound on
the number of program variables from the invariant, is interesting
further work, with connections to the inverse problem of
difference Galois theory [1]}.
