Tips for finding Loop Invariants

TL;DR: Short Summary

• Tip 1: invariant must contain variable we operate on and must be as precise as possible
• Tip 2: "loop-carried" variables must be included in the loop invariant
• Tip 3: create generalized tables to visualize the connections between variables inside the loop
• Tip 4: there must be a relation between the variables needed to calculate x$x$ in the loop and after the loop
• Tip 5: if the loop condition contains inequality, the counter should be "limited on the opposite side" in order to reach equality
• Tip 6: if certain program inputs are restricted, these restrictions about input variables should be included in the loop invariant
• Tip 7: if the variable in our loop invariant depends on some other value, it needs to be included in some way in our loop invariant
• Tip 8: when proving termination, r$r$ must be included in the loop invariant
• Tip 8.5: when proving termination, all variables required for calculating r$r$ must be included in the loop invariant

Detailed Tips

• Tip 1: invariant must contain variable we operate on and must be as precise as possible

  • example:
    • i \geq 0$i \geq 0$ would be a bad invariant, since we cannot imply x = 2n$x = 2n$
    • similarly, x \geq 0$x \geq 0$ would also be a bad invariant, since we still cannot imply x = 2n$x = 2n$
    • x = 2i$x = 2i$, however, would suffice
      

• Tip 2: "loop-carried" variables (variables which depend on their value from the previous loop iteration) must be included in the loop invariant

  • example:
    • x = \sum_{k=0}^i3k$x = \sum_{k=0}^i3k$ would be a bad invariant, since we know nothing about y$y$
    • x = \sum_{k=0}^i3k \land y = 3i$x = \sum_{k=0}^i3k \land y = 3i$ would work, however
      
    • if, instead, y$y$ was not dependent on its previous value, x = \sum_{k=0}^i3k$x = \sum_{k=0}^i3k$ would suffice
      

• Tip 3: create generalized tables to visualize the connections between variables inside the loop

  • example:
    • we see that y = i!$y = i!$ and x = 2\sum_{k=0}^ik!$x = 2\sum_{k=0}^ik!$
      
    • as such, a good invariant would be the conjunction of these two, namely x = 2\sum_{k=0}^ik! \land y = i!$x = 2\sum_{k=0}^ik! \land y = i!$
      

• Tip 4: there must be a relation between the variables needed to calculate x$x$ in the loop and after the loop

  • example:
    • x = 2i^2 - 32$x = 2i^2 - 32$ cannot imply 2n^2 + 16|n|$2n^2 + 16|n|$; there needs to be some connection between n$n$ and i$i$ or k$k$
    • we see that k = |n| + 4$k = |n| + 4$, and incorporating this into our loop invariant would allow us to make the needed connection (I \equiv k = |n| + 4 \land x = 2i^2 - 32$I \equiv k = |n| + 4 \land x = 2i^2 - 32$)
      

• Tip 5: if the loop condition contains inequality, the counter should be "limited on the opposite side" in order to reach equality (e.g. if i$i$ is decremented, include i \geq 0$i \geq 0$, else if i$i$ is incremented, include i \leq n$i \leq n$)

  • example:
    • compared to previous examples, x = 2i$x = 2i$ would not suffice, since we cannot imply that i \geq n$i \geq n$ (we need to show that, at that moment, i = n$i = n$ holds)
    • we make our assertion stronger: (i < n \land x = 2i) \lor (i \geq n \land x = 2n) \Longleftarrow (i < n \land x = 2i) \lor (i = n \land x = 2n)$(i < n \land x = 2i) \lor (i \geq n \land x = 2n) \Longleftarrow (i < n \land x = 2i) \lor (i = n \land x = 2n)$
    • eventually, we reach x = 2i \land i \leq n$x = 2i \land i \leq n$, but x = 2i$x = 2i$ still does not imply this assertion, meaning we must include i \leq n$i \leq n$ in our assertion (I \equiv x = 2i \land i \leq n$I \equiv x = 2i \land i \leq n$)
      

• Tip 6: if certain program inputs are restricted (e.g. having to take the absolute value of an input n$n$ to only allow positive integers), these restrictions about input variables should be included in the loop invariant

  • example:
    • this program doesn't work for some negative n$n$...
      
    • as such, some construct is most likely included before the loop to handle problematic inputs, which must be accounted for in the loop invariant
      

• Tip 7: if the variable in our loop invariant depends on some other value, it needs to be included in some way in our loop invariant - if the value constantly fluctuates between one value and another, a simple formula will do, otherwise, do case-by-case if-then-else analysis (e.g. (c1 \implies ...) \land ... \land (c_n \implies ...)$(c1 \implies ...) \land ... \land (c_n \implies ...)$)

  • example:
    • x$x$ is dependent on the value b$b$, which is either 0$0$ or 1$1$ in any iteration (but 0$0$ when we're done)
    • as such, a simple formula I \equiv x = 4i + b$I \equiv x = 4i + b$ suffices
      

• Tip 8: when proving termination, r$r$ must be included in the loop invariant

• Tip 8.5: when proving termination, all variables required for calculating r$r$ must be included in the loop invariant