Loop invariant checking should assert that if the invariant is true before the loop starts, it will also be true at the end of the loop. That’s not a general ca

Loop invariant checking should assert that if the invariant is true before the loop starts, it will also be true at the end of the loop. That’s not a general capability of assert constructs.