What is the best way of determining a loop invariant?
It has already been pointed out that one same loop can have several invariants, and that Calculability is against you. It doesn’t mean that you cannot try. You are, in fact, looking for an inductive invariant: the word invariant may also be used for a property that is true at each iteration but for which is … Read more