Loop invariant vs Assertions

algorithmsinvariantsloopspseudocode

I have an exam on Programming Concepts this Saturday and I am struggling to find some information to understand some concepts better.

What is the difference between loop invariant and assertion? To me they look the same.

Also, what exactly is while loop invariance theorem?

Not sure whether it is me or it is ridiculously hard to find any specific information about algorithms and pseudocode online.

Best Answer

An invariant is a condition that can be relied upon to be true during execution of a program. For example, a loop invariant is a condition that is true at the beginning and end of every execution of a loop.

An assertion is a predicate (a true–false statement) placed in a program to indicate that the developer thinks that the predicate is always true at that place. Programmers often use assertions in their code to make invariants explicit.

While Loop Invariance Theorem
Assume that S is an invariant of the loop

While C do
 E

Assume also that S is true on the first entry to the loop. Then S stays true after every iteration of the loop. In particular,

  1. If the loop terminates then S is true after the last iteration.
  2. If the loop does not terminate then S always stays true.
Related Topic