[fishstock25]

Another way to view such invariant is to see it as a generalization of both pre- as well as post-condition.

The pre-condition is a special case, then the invariant provides the "guard rails" along which the computation proceeds, and then the post-condition is again a special case which ultimately is the result of the computation.

In the search example of the computation, the pre-condition is "the position is somewhere in the allowed indices", the post-condition is "the return value is the position". The stated invariant is "the value is between current min and max bounds". These bounds become tighter and tighter, so that eventually the pre-condition is transformed into the post-condition.