Nice idea of check your program - try to prove your program is correct

Come to think of it - that's how I got my today's bubble sort worked.  In fact, a loop variant proof usually give extra insight to how the algorithm works.