Termination is not about the loop invariant.  You also need a measure of termination, which is usually a nonnegative integer which decreases on each iteration.<p>In our Pascal-F system, we had a MEASURE statement for that. You didn&#x27;t need it for FOR loops, though.