Question

Find a loop invariant (I) for the following while loop with the post-condition

{Q: S=1}, where S is an integer and the operator / represents an integer division.

Show your work step by step to receive full credit.

         while (S > 1) do
              S = S / 2;
         }

Answer 1

Loop invariant can be defined as a condition which will always be true. This property must be satisfied throughout every iteration of the loop.

We have the post-condition:

Q: S = 1

The given loop checks if the value of 'S' is greater than 1 or not. If it is true, then it divides 'S' by 2 and this process is repeated in every iteration. The while loop condition will fail when the value of 'S" is one or less. At that case, the value of 'S' will never be less than one as it is integer in nature. Loop invariant does not depend on the state of the iterative condition. It always remains true irrespective of the iterative condition which can be true or false.

The post-condition must be true after the execution of the while loop condition.

So, one loop invariant we can determine from the given relation is:

S > 1 [the while loop will be executed only when 'S' is greater than one, not equal to one]

Please comment in case of any doubt.
Please upvote if this helps.