raptors892004 wrote:
... four steps to develop a loop from a loop invariant...
Interesting. So you are saying that given a loop invariant, you want to develop/implement a loop that satifies the invariant?
Quote:
1.Set initial values for any loop control variables.
2. Determine the condition that causes the loop to terminate.
3. Modify the control variable(s) so the loop progresses toward termination.
4. Check that the invariant remains true at the end of each iteration.
Assuming a response in the affirmative to the above question, these steps are probably okay--but they are less steps, but more things you have to consider. In fact, you need the first three for practically any loop.
"Step 4" is actually much more than it can appear to be. The key could be to consider what side-effects the loop should have (if any) such that the invariant will be true at the end of each iteration. (As far as I know, it should also be true going into the loop--that is, true before the loop starts).
Quote:
Another thing the slideshow said is that invariants should be used to test programs thoroughly.
That is where the bit about the "assertions" comes from in my previous response.