Methods for designing loops

The method for designing loops is to ask two questions: will it always end, and whenever it terminates, will the data meet the conditions required?

In the CATMOUSE example, the loop terminates (and the game ends) when:
  1. The mouse runs to the hole.
  2. The mouse runs into the cat.
  3. The cat catches the mouse.