Prove the following program is correct n 0 count n sum 0

Prove the following program is correct: {n > 0} count = n; sum = 0; while count 0 do sum = sum + count; count = count - 1; end {sum = 1 + 2 +. .. + n}

Solution

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

Given code:

   {n>0}
   count =n;
   sum =0;
  
   while count<> 0 do
       sum = sum + count;
       count = count-1;
   end
   {sum = 1+2+...+n}
  
Lets start with example

Taking n = 5 , a positive number n>0}
count=5
sum =0

   while count <> 0 do here 5 <> 0 correct
       sum = sum + count;
       sum = 0 + 5;
       sum = 5
       count = count-1;
       count = 5-1;
       count = 4;
      
   while count <> 0 do here 4 <> 0 correct
       sum = sum + count;
       sum = 5 + 4;
       sum = 9
       count = count-1;
       count = 4-1;
       count = 3;
  
   while count <> 0 do here 3 <> 0 correct
       sum = sum + count;
       sum = 9 + 3;
       sum = 12
       count = count-1;
       count = 3-1;
       count = 2;

   while count <> 0 do here 2 <> 0 correct
       sum = sum + count;
       sum = 12 + 2;
       sum = 14
       count = count-1;
       count = 2-1;
       count = 1;

   while count <> 0 do here 1 <> 0 correct
       sum = sum + count;
       sum = 14 + 1;
       sum = 15
       count = count-1;
       count = 1-1;
       count = 0;

   while count <> 0 do here 0 <> 0 incorrect
  
  
Final sum value is 15 which is expected value of {1+2+3+4+5 = 15}

Hence the given program is correct.
=======================================================================