Invariants
definition:
something that stays true during the execution of an algorithm
in practice, is a condition/fact/property that:
- may become false, but is then made true again
- is exploited by the algorithm
exploited = sfruttato
example: sum of an array
obvious algorithm:
s = 0
for (i = 0; i < lenght; i++)
s = s + v[i];
invariant:
s is always equal to v[0]+…+v[i]
is it always true?
- if it becomes false, is made true again?
- is exploited?
point 1: if it becomes false…
become false = was true, now false
example: i was 3
| v[0] |
|
|
| v[1] |
| |
| v[2] |
| = s |
| i=3 | v[3] |
|
|
| v[4] | | |
v[0] -+
v[1] |
v[2] | = s
i=3 v[3] -+
v[4]
invariant was true means:
s == v[0] + v[1] + v[2] + v[3]
does it ever become false?
point 1: the invariant becomes false
execute only the single instruction i++
i changes from 3 to 4
everything else stays the same
| v[0] |
| |
| v[1] |
| |
| v[2] |
| = s |
| v[3] |
| |
| i=4 | v[4] | | |
v[0] -+
v[1] |
v[2] | = s
v[3] -+
i=4 v[4]
s is not changed by i++ alone
is still v[0]+v[1]+v[2]+v[3]
s is not equal to
v[0]+v[1]+v[2]+v[3]+v[4]
the invariant is no longer true
why:
the invariant is s == v[0]+…+v[i]
and i is now 4
point 1: restore the invariant
an invariant may become false
but is made true again
| s is | v[0]+v[1]+v[2]+v[3] |
| should be | v[0]+v[1]+v[2]+v[3]+v[4] |
how to restore?
v[0]+v[1]+v[2]+v[3]+v[4] is the equal to
(v[0]+v[1]+v[2]+v[3])+v[4], which is equal to
s + v[4]
s is not right
should be equal to s + v[4]
fix: make s equal to s + v[4]
| v[0] |
| |
| v[1] |
| |
| v[2] |
| = s |
| v[3] |
| |
| i=4 | v[4] | | |
|
⇒ |
| v[0] |
| |
| v[1] |
| |
| v[2] |
| = s |
| v[3] |
| |
| i=4 | v[4] |
| |
|
v[0] -+ v[0] -+
v[1] | v[1] |
v[2] | = s => v[2] | = s
v[3] -+ v[3] |
i=4 v[4] i=4 v[4] -+
point 1: restore the invariant, in general
| v[0] |
| |
| v[1] |
| |
| v[2] |
| = s |
| i=3 | v[3] |
| |
| v[4] | | |
|
⇒ |
| v[0] |
| |
| v[1] |
| |
| v[2] |
| = s |
| v[3] |
| |
| i=4 | v[4] | | |
|
⇒ |
| v[0] |
| |
| v[1] |
| |
| v[2] |
| = s |
| v[3] |
| |
| i=4 | v[4] |
| |
|
v[0] -+ v[0] -+ v[0] -+
v[1] | v[1] | v[1] |
v[2] | = s => v[2] | = s => v[2] | =s
i=3 v[3] -+ v[3] -+ v[3] |
v[4] i=4 v[4] i=4 v[4] -+
initially i=3
s is v[0]+…+v[i]
i is increased
invariant falsified
restore: s = s + v[i]
point 2: exploited?
at every execution of i++:
was true before ⇒ can be made true again
if it was not true, it cannot be restored
| v[0] |
| |
| v[1] |
| |
| v[2] |
| ≠ s |
| i=3 | v[3] |
| |
| v[4] | | |
v[0] -+
v[1] |
v[2] | != s
i=3 v[3] -+
v[4]
if s is not equal to v[0]+v[1]+v[2]+v[3]
s = s+v[4] does not make it equal to v[0]+v[1]+v[2]+v[3]+v[4]
If the invariant were not true before i++, increasing s would
not make it true. This is the first use of the invariant: it is necessary to
make it true again.
point 2: other than staying true?
looks pointless:
invariant used to restore itself
at the end: i is equal to the length of the array
invariant: s = v[0] + … + v[lenght-1]
s is the sum of all elements of the array
invariant true = problem solved
everyone knows how to sum an array!
not in programming 101
algorithms can be far more complex
easy to get confused about what to do at some point
- invariants guarantees the correctness of algorithms
- can be used to think locally to obtain global results
how programmers think
- I start here
- I enter the loop
- when I am at the i-th iteration I do this
- at this point I get out of the loop
common mistake:
at the i-th iteration, use some assumption
do not ensure it is still true before the i+1-th iteration
Many programs are so algorithmically simple that they do not require any of
this. Making invariants explicit is relevant to programs that have complex
loops, where several variables interact in a non-trivial way.
use of invariants
made true at the beginning
if become false, they are restored
at the end, allow obtaining the result
like the induction principle
true for n=0
if true for n, is true for n+1
instead of mentally unrolling the cycle
make sure that was is exploited is made true again
does not require simulating the whole algorithm
requires thinking about a single iteration
The induction principle in mathematics allow proving a property for all values
of a number
n. Instead of proving the property for every number
n, it works by proving the property for
0, and then proving
that if the property obtains for
n, it also obtains for
n+1.
In programming, allows concentrating on a single iteration of the loop. If the
invariant is initially true, and is restored whenever is falsified during a
single iteration, then it is true at the end.
nobody uses invariants while programming
simple algorithms do not require them
note: long program ≠ complex algorithm
if a condition that is used becomes false, program fails
programmers fix the problem by making it true again
invariants used, but not explictly
Everyone who has implemented a non-trivial algorithm has met the concept of
invariants, knowingly or not, when fixing a loop where the problem was of a
wrong interaction between an iteration and the next.
invariants in searching
what changes in A*:
- inner (=closed) and frontier nodes
- table of values d(n)
only three data structures
yet, lot of wrong implementations
in spite of relative simplicity of the algorithm
(only two nested loops)
variants of A*
making some invariant explicit allows for variants
changing the value of n→m falsify the invariant
can be made true again
Making an invariant explicit allows for a better understanding of how an
algorithm works. Sometimes it even allows for improvements or variants.