MHB Is there also an other way to prove the sentence?

[evinda]

Hello! (Wave)

I am looking at the algorithm of the insertion sort:

     Input: A[1 ... n]     for j <- 2 to n
        key <- A[j]
        i <- j-1
        while (i>0 and A[i]>key)
              A[i+1] <- A[i]
              i <- i-1
        end
        A[i+1] <- key
     end

There is the following sentence:

At the beginning of each iteration "for" ,the subsequence $ A[1 \dots j-1]$ consists of the elements that are from the beginning at these positions, but sorted with the desired way.

I found the following proof in my textbook:

• Initial control, when $j=2:$
  The sentence is true,because the subsequence $A[1]$ is sorted in a trivial way.
  
• Preservation control:
  The algorithm moves the elements $ A[j-1], A[j-2], \dots $ to the right side,till the right position for $ A[j] $ is found.
  
• Verification of the result:
  When the loop "for" ends, $j$ has the value $n+1$. The subsequence is now $ A[1 \dots n]$, which is now sorted.
  

But...could you tell me if there is also an other way to prove the sentence? (Thinking)

 

[Evgeny.Makarov]

could you tell me if there is also an other way to prove the sentence?

Using a loop invariant is the usual way of proving that a loop performs a desired action. What don't you like about it and why do you want another proof?

 

[evinda]

Using a loop invariant is the usual way of proving that a loop performs a desired action. What don't you like about it and why do you want another proof?

The proof is nice,I just wanted to know of the there is an other way to prove it,rather than using indunction.. (Thinking)