Figure REF  overviews our
approach towards synthesising loops and/or their invariants.
In order to generate invariants, we extract a system of C-finite recurrence
equations describing loop updates.
We then compute the polynomial ideal, called the polynomial invariant
ideal, containing all
polynomial equality invariants of the loop, by using recurrences
solving and Gröbner basis computation [1]}.
Any polynomial invariant of the given loop is then a logical
consequence of the polynomials from the computed polynomial ideal basis [2]}.
On the other hand, for loop synthesis, we take a basis of
the polynomial invariant ideal generated by given polynomial loop invariants and
construct a polynomial constraint problem. This constraint problem precisely
characterises the set of all C-finite recurrence systems for which the
given polynomial invariants yield algebraic relations among the
induced
C-finite number sequences. Every
solution of the constraint problem gives thus rise to a system of
C-finite recurrence equations, which
is then turned into a loop for which the given polynomial relations
are
loop invariants [3]}.
