-
Tip 1: invariant must contain variable we operate on and must
be as precise as possible
- example:
- i \geq 0i≥0 would be a
bad invariant, since we cannot imply x = 2nx=2n
- similarly, x \geq 0x≥0 would also be
a bad invariant, since we still cannot imply x = 2nx=2n
- x = 2ix=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}^i3kx=∑k=0i3k
would be a bad invariant, since we know nothing about yy
- x = \sum_{k=0}^i3k \land y = 3ix=∑k=0i3k∧y=3i
would work, however
- if, instead, yy
was not dependent on its previous value, x =
\sum_{k=0}^i3kx=∑k=0i3k
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∑k=0ik!
- as such, a good invariant would be the conjunction of these two,
namely x = 2\sum_{k=0}^ik! \land y = i!x=2∑k=0ik!∧y=i!
-
Tip 4: there must be a relation between the variables needed to calculate xx in the
loop and after the loop
- example:
- x = 2i^2 - 32x=2i2−32 cannot imply
2n^2 + 16|n|2n2+16∣n∣; there needs
to be some connection between nn and
ii or
kk
- we see that k = |n| + 4k=∣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 -
32I≡k=∣n∣+4∧x=2i2−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 ii is decremented,
include i \geq 0i≥0, else if ii is incremented,
include i \leq ni≤n)
- example:
- compared to previous examples, x = 2ix=2i
would not suffice, since we cannot imply that i \geq
ni≥n (we
need to show that, at that moment, i = ni=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∧x=2i)∨(i≥n∧x=2n)⟸(i<n∧x=2i)∨(i=n∧x=2n)
- eventually, we reach x = 2i \land i \leq nx=2i∧i≤n,
but x = 2ix=2i
still does not imply this assertion, meaning we must include i \leq
ni≤n in
our assertion (I \equiv x = 2i \land i \leq nI≡x=2i∧i≤n)
-
Tip 6: if certain program inputs are restricted (e.g. having to
take the absolute value of an input nn 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 nn...
- 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⟹...)∧...∧(cn⟹...))
- example:
- xx is
dependent on the value bb,
which is either 00 or 11 in any
iteration (but 00 when we're
done)
- as such, a simple formula I \equiv x = 4i + bI≡x=4i+b
suffices
-
Tip 8: when proving termination, rr
must be included in the loop invariant
-
Tip 8.5: when proving termination, all variables required for
calculating rr must be
included in the loop invariant