More on iteration

The 3-hour night version lecture is a real torture. For the example counter(m,n), i can't relate the loop invariant directly to the correctness of the program. It's weird that the b value is set to 6.
I tried pick two non-zeros natural numbers for m and n randomly. And the loop has to execute 6 more times to terminate after a and b decrease to 0 since b is assigned to 6 and c has to counter 6 more times. It may be necessary to use the loop invariant c = 7m + n to go to the postcondition, but it seems not to be that straightforward to be understood. Now i realize the importance of code design that make other people's life easier, for people who are learning how to prove loop invariant. Back to the loop invariant, i usually trace algorithm on simple example, like iterates for a few times and see what kind of changes are caused. As to me it's more helpful than just thinking of some fancy relationship between precondition and postcondition.
For more complicated loops, like nested loops, these things have to be done inside out. Prove termination and loop invariant in the very inside, then for any value of the loop outside, prove termination and loop invariant for outside loop. In the selection_sort example, the inside loop is going from index j=i+1 to the end of the list. Selection_sort is basically "selecting" a proper position for an element in the unsorted section of that list. I take a [4,2,3,1] as an example to run the loop. The inside loop actually helps me to evaluate a position by comparing the value of 4 to 2,3 and 1, then the outer loop moves to the next index and this easily sorts the whole list. But the inside loop may have k+1 iteration or may not. Since the value of the number could be equivalent. These "special" cases happened because of the postcondition, which is non-decreasing order here. Then it's not hard to prove the program "moves" and "compares" in some range.