2
$\begingroup$

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Here is an small example where I got stuck several times, the example is a sub problem that I skinned out for solving insertion sort algorithm.

/**
 * Inserts the given value in proper position in the array.
 * @param array
 * @param rightIndex The index till which sub array is sorted.
 * @param value The value to be inserted into sorted sub array.
 */
function insert(array, rightIndex, value) {
    // assert sorted(array, rightIndex)
    for(var j = rightIndex; j >= 0 && array[j] > value; j--) {
        array[j + 1] = array[j];
    }   
    array[j + 1] = value;
    // assert sorted(array, rightIndex+1) 
};

The mistakes that I did initially were:

  1. Instead of j >= 0 I kept it j > 0.
  2. Got confused whether array[j+1] = value or array[j] = value.

That time I don't have any tool to verify where I am doing wrong, fortunately on Googling I came to know about loop invariants.

To get hold of the above concept I thought to apply the concept here, although I am not mathematician but trying some equation I thought this would be good invariant.

$$array[0...j] <= val < array[j+2...rightIndex+1]$$

As far as I understood the concept, its a loop invariant because the inequalities contains the loop variable j. How to utilize this equation here?

Being naive at this concept I am stuck and don't know how to use this invariant in my loop. How to gain confidence about the correctness of my loop?

$\endgroup$
  • $\begingroup$ I'm not sure I understand what you are asking. Use the loop invariant for what purpose? What are you trying to accomplish? Loop invariants are often used to verify that your code is correct. Is that what you're trying to achieve? $\endgroup$ – D.W. Apr 17 '16 at 7:14
  • $\begingroup$ @D.W. see the mistakes that I did, I want to avoid those silly mistakes in future so that I can concentrate on original problem. $\endgroup$ – CodeYogi Apr 17 '16 at 7:21
  • $\begingroup$ I encourage you to edit the question to be more explicit about what you're trying to achieve and what your goals are. "How to utilize this equation here" - for what? 'how to move forward' - move forward at what? 'How to get hold of the concept of...' - not clear to me what that means. See if you can edit the question to articulate more clearly exactly what you want an answer to. Thank you! $\endgroup$ – D.W. Apr 17 '16 at 7:24
  • $\begingroup$ Also posted on Programmers. Please don't do this. I think it makes sense to ask about loop invariants both to programmers and to computer scientists — but your question must be tailored to each site: computer scientists don't care about competitive programming, for instance. $\endgroup$ – Gilles Apr 18 '16 at 17:14
  • $\begingroup$ @Gilles corrected, basically I wanted to know how different communities think of the same but important problem. $\endgroup$ – CodeYogi Apr 18 '16 at 17:27
2
$\begingroup$

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ⱼ < aⱼ₋₁? Then we can obtain the needed condition by swapping the indices and so the loop body becomes

if aⱼ < 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ⱼ < aⱼ₋₁ then swap(j, j-1);
   j ≔ j - 1

That is,

aᵣ₊₁ ≔ e;
for(int j = 0; 0 < j; j--)
   if aⱼ < 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 < j; j--)
   if aⱼ < aⱼ₋₁ then swap(j, j-1) else return;

Hope this helps!

$\endgroup$
  • 1
    $\begingroup$ Efficiency be damned. I like this last loop because it's clear. Makes it easy to spot that jstarts at 0 and we never loop. Even if we did it's all downhill from here. Consider adding some knowledge about the size of the sorted part of the array. Previously called rightIndex $\endgroup$ – candied_orange Apr 18 '16 at 21:49
  • $\begingroup$ The initialization of j seems wrong in the last loop, it should be int j = r+1. $\endgroup$ – CodeYogi Apr 26 '16 at 8:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.