Let us first motivate loop synthesis using Figure REF . The loop is
based on an online tutorialhttps://rise4fun.com/Dafny/ of the
Dafny verification framework [1]}: Figure REF  uses only
affine updates among its variables, and the task is to revise/repair
Figure REF  into a partially correct program with respect to the
precondition \(N\ge 0\)  and post-condition \(c=N^3\)  such that the polynomial loop
invariant \(n \le N \wedge c=n^3 \wedge k=3n^2+3n+1 \wedge m=6n+6\)  holds. We note that our focus in on partially correct programs [2]}, and thus we do not consider total correctness, that is loop termination.
<FIGURE>