The following questions refer to the code shown below count

The following questions refer to the code shown below count = n; sum = 0; while count 0 do sum = sum + count; count = count - 1; end {sum = 1 + 2 + ... + n} What is the weakest precondition for this code and the given postcondition? Give an invariant that is strong enough to prove the partial correctness of the loop. Make your invariant as weak as possible. Give an invariant that is strong enough to prove the total correctness of the loop.

Solution

==================================================================\\
---------------
Answer:
---------------

Given Code

   count = n;
   sum = 0;
   while count <> 0 do
       sum = sum + count;
       count = count -1;
   end
   {sum = 1+2+...+n}
  
a)   count==0
  
   count ==0 is the weakest invariant in the loop where the loop terminates at some iteration as the count value
   decreases by 1 for each iteration.
  
b)   count!=0
  
   count! = 0 is the strong invariant so that it can pass each iteration.
   But in some cases if inner loop computes to negative value of count this might fail.
   Hence we can say its partial correctness of the loop.
  
c)   count>0

   count>0 is the strong invariant hence it will prove the total correctness of the loop.
   So by making count!=0 to count>0 will give total correctness of the loop.
  
==================================================================