How to use the concept of loop invariant to reduce errors in loops?
I'm not terribly familiar with the topic, and as such let's discuss a simpler
variation of your problem. In particular, rather than consider a sorted subarray,
let's suppose our function is given a sorted array instead.



So we are given a value e and a sorted array a[0..r], and our goal
is to have the array a[0..r+1] sorted after insertion of e. For reference, let us
introduce some abbreviations.

$$ Sorted \; a[m..n] ∶≡ (∀ i : m..n • aᵢ ≤ aᵢ₊₁) $$

Now our program has precondition and post-condition

Pre : Sorted a[0..r] ∧ a = A₀
Pos : Sorted a[0..r+1] ∧ e ∈ a[0..r+1] ∧ a is a permutation of A₀ with e inserted


The A₀ is used to make sure that no elements of a are deleted or rewritten;
indeed, setting all elements of the array to e gives us a sorted array that contains
e! But we can simplify matters by simply putting a constraint on the code:
only array swaps are allowed.

Pre : Sorted a[0..r] 
Pos : Sorted a[0..r+1] ∧ e ∈ a[0..r+1]


Now a usual way to obtain an invariant from the post-condition is to replace a constant with
a variable and adding an equality to regain the post-condition, so let's try replacing 0 in Pos with j
and add an equality for the two:

Sorted a[j..r+1] ∧ e ∈ a[j..r+1] ∧ j ≈ 0


This clearly establishes the post-condition, so we're on the right track!
Let's simplify it further by breaking the equality up:

Sorted a[j..r+1] ∧ e ∈ a[j..r+1] ∧ j ≤ 0 ∧ 0 ≤ j


Now half of this is easily made-true by taking j ≔ r+1 and aᵣ₊₁ ≔ e
---since Sorted a[r+1..r+1] ≡ aᵣ₊₁ ≤ aᵣ₊₁ and e ∈ a[r+1..r+1] ≡ aᵣ₊₁ ≈ e---
and thus this half we take to be the invariant

P : Sorted a[j..r+1] ∧ e ∈ a[j..r+1] ∧ 0 ≤ j


and the rest we take to be the negation of the loop guard, and so our loop has condition

B : 0 ≤ j - 1


Summarizing so far:
if our loop has guard B and invariant P, then if the loop terminates we must have
the guard is false and the invariant still holds, ie
$Sorted\; a[j..r+1] ∧ e ∈ a[j..r+1] ∧ j ≤ 0 ∧ 0 ≤ j$, and from this the post-condition is
established!

To continue the derivation of our program, we need to the loop (whatever it is, since we have
not yet found it) to terminate, since the above summary said if the loop terminates.
The guard gives us that j is a positive value and so a good
candidate for a bound on the number of iterations in the loop.
It can be decreased by each iteration of the loop by incrementing it, j ≔ j -1, and so that is what we try do.

Of course the invariant, by definition, must be left-true by the body of the loop.
In particular, assuming the invariant and the guard, we must show that the invariant still holds
after execution of the proposed loop-body j ≔ j -1.

  P still holds after execution of j ≔ j - 1
≡⟨ definitions ⟩
  Sorted a[j-1..r+1] ∧ e ∈ a[j-1..r+1] ∧ 0 ≤ j-1
≡⟨ 0 ≤ j - 1 follows from B ⟩
  Sorted a[j-1..r+1] ∧ e ∈ a[j-1..r+1]
≡⟨ e ∈ a[j-1..r+1] ≡ e ≈ aⱼ₋₁ ∨ e ∈ a[j..r+1], and this follows from P ⟩
  Sorted a[j-1..r+1]
≡⟨ By P we know that Sorted a[j..r+1], 
   so a[j-1..r+1] is sorted precisely when aⱼ₋₁ ≤ aⱼ ⟩  
  aⱼ₋₁ ≤ aⱼ


So we need the decrement to be guarded by this condition.
But what if this condition does not hold; ie instead we have aⱼ &lt; aⱼ₋₁?
Then we can obtain the needed condition by swapping the indices and so
the loop body becomes

if aⱼ &lt; aⱼ₋₁ then swap(j, j-1);
j ≔ j-1;


So we've obtain a terminating loop and so our summary above means we are done.
So the resulting program is:

j ≔ r+1;
aᵣ₊₁ ≔ e;
while 0 ≤ j - 1:
   if aⱼ &lt; aⱼ₋₁ then swap(j, j-1);
   j ≔ j - 1


That is,

aᵣ₊₁ ≔ e;
for(int j = 0; 0 &lt; j; j--)
   if aⱼ &lt; aⱼ₋₁ then swap(j, j-1);




Let's try it out.

Given sorted array a = [1,2,3,4,5] and value e = 3
we get $r = 5$ and so, letting | denote where we are looking
in the array, the loop looks as follows:

j  a
6  [1,2,3,4,5 | 3]
5  [1,2,3,4 | 3,5]
4  [1,2,3| 3,4,5]
3  [1,2| 3,3,4,5]
2  [1| 2,3,3,4,5]
1  [|1, 2,3,3,4,5]


In particular, note that since the array is initially sorted, the moment
we stop making swaps we no longer make any swaps at all and just decrement
the counter. With this mind, we can be a bit perverse (for the sake of efficiency?)
and write

aᵣ₊₁ ≔ e;
for(int j = 0; 0 &lt; j; j--)
   if aⱼ &lt; aⱼ₋₁ then swap(j, j-1) else return;




Hope this helps!