Hi Ranjit,

I would suggest starting from the post-condition as you will have to derive that the post-condition is true if the invariant evaluates to true inside the loop and the loop condition evaluates to false. So, the post-condition should have some relation to these two terms. Next, you will have to ensure that you may derive validity of the invariant before the loop is executed the first time from the pre-condition. So post- and pre-condition give you the building blocks. Nevertheless, in most cases, you will have to 'play around' with them to find a recombination that is actually invariant when executing the instructions in the loop. I'm afraid this is sort of a question of experience. There is no general recipe.

Greetings,

Jörg

Each loop has its programming logic. Just to avoid infinite loops, use a boolean variable that takes the value "False" if there is no assignment to exit the loop.

I would say go through this list when you design the loop

What initialization is necessary for the loop’s test expression?

What initialization is necessary for the loop’s processing?

What causes the loop to terminate?

What actions should the loop perform?

What actions are necessary to prepare for the next iteration of the loop?

What conditions are true and what conditions are false when the loop is terminated?

When the loop completes what actions are need to prepare for subsequent program processing?

But again you'll still have to work around with trial and error method to fine tune the loop and ensure correctness.

Look at the loop and try to say in most general words, what does it do. Then, try to describe in general words, how main variables are changing. The key words are "most general". And, of course, invariant must be consequent with pre- and postcondition.

For more information read David Gries The Science of Programming.

Good luck,