Introduction

Insertion sort is one of the simplest sorting algorithms. It is quite
efficient for small arrays. Its runtime increases with the square of the
number of elements to be sorted. Therefore it should not be used with large
data sets. For large data sets algorithms like merge sort or heap sort are far
more efficient.

All sort algorithms work on abstract arrays. An abstract array can have
different implementations. The sort algorithm just need random access to the
elements.

An abstract array has the following interface.

 deferred class
 ABSTRACT_ARRAY[G]
 feature
 content: ghost LIST[G]
 count: NATURAL
 deferred
 ensure
 Result = content.count
 end
 [](i:NATURAL)
 require
 i < count
 deferred
 ensure
 Result ~ content[i]
 end
 swap(i,j:NATURAL)
 require
 i < j
 j < a.count
 deferred
 ensure
 a.content = old a.content.swapped(i,j)
 end
 end

For the purposes of sorting we need access only to the content (ghost access
is sufficient), the length of the array, the individual elements in a random
access manner. The only procedure we need is to swap two elements.

Needed list functions

The ghost function “content” returns the elements as a list. This function is
needed to describe the properties well. We never need the list in actual
computations. But the data type is such a powerful type that it can serve as a
“swiss army kife” in many algorithms. The following subsections describe what
properties are needed from lists.

Univerally quantified expressions

If we need to verify that all elements of the concatenation of two lists “u+v”
satisfy a certain condition “e”, then it is sufficient to prove that all
elements of the lists “u” and “v” individually satisfy the corresponding
condition.

 all(u,v:LIST[G], a:G, e:BOOLEAN)
 require
 all(x:G) x in u => e
 all(x:G) x in v => e
 e[x:=a]
 ensure
 all(x:G) x in (u+v) => e
 all(x:G) x in (u+a) => e
 all(x:G) x in (a::u) => e
 end

Take and drop

The function “l.take(i)” returns a list with the first “i” elements of the
list “l” or the whole list in case that “i” exceeds the number of elements in
the list. “l.drop(i)” returns the list “l” where the first “i” elements have
been removed. The functions “take” and “drop” satisfy the following properties.

 all(l:LIST[G], i:NATURAL)
 ensure
 l.take(i).count = min(i,l.count)
 l.take(i) + l.drop(i) = l
 l.take(l.count) = l
 l.drop(l.count) = nil
 i/=0 => i<=l.count
 => l.take(i) = l.take(i-1) + l[i-1]
 i<l.count
 => l.drop(i) = l[i]::l.drop(i+1)
 i/=0 => i<l.count
 => l = l.take(i-1) + l[i-1]::l[i]::l.drop(i-1)
 end

Tail zipping

A list can be zipped with its own tail. Tail zipping enjoys the following
properties.

 all(u,v:LIST[G], e1,e2:G)
 ensure
 nil.tail_zipped = nil
 (e1::nil).tail_zipped = nil
 (e1::e2::u).tail_zipped = [e1,e2]::(e2::u).tail_zipped
 u=nil => (u+v).tail_zipped = v.tail_zipped
 v=nil => (u+v).tail_zipped = u.tail_zipped
 (u+e1+v).tail_zipped = (u+e1).tail_zipped + (e1::v).tail_zipped
 u/=nil
 => v/=nil
 => (u+v).tail_zipped
 = u.tail_zipped + [u.last,v.first] + v.tail_zipped
 end

Example:

 ([1,2,3,4]).tail_zipped = [[1,2],[2,3],[3,4]]

A list is sorted if in the tail zipped list all tuples have a first component
which is less or equal than its second component.

Swapping

The expression “l.swapped(i,j)” returns a list which is equal to “l” except
that the elements in position “i” and “j” are swapped.

 swapped:
 all(l:LIST[G], j:NATURAL)
 require
 j /= 0
 j < l.count
 ensure
 swap1: l.swapped(j-1,j).is_permutation(l)
 -- "is_permutation" is an equivalence relation
 swap2: l.swapped(j-1,j).take(j-1) = l.take(j-1)
 swap3: l.swapped(j-1,j).drop(j) = l[j-1]::l.drop(j+1)
 swap4: l.swapped(j-1,j).drop(j-1) = l[j]::l[j-1]::l.drop(j+1)
 end

The insertion sort algorithm

The algorithm starts with an empty prefix of the content. An empty list is
always sorted. Then it loops over all elements successively and inserts the
new elements into the correct position of the already sorted prefix of the
list. The algorithm terminates if all elements are inserted at their proper
location.

We put the needed functions and procedures in a module “insertion_sorter”.

 -- module: insertion_sorter
 immutable class
 INSERTION_SORTER[G:ORDER]
 end

The class INSERTION_SORTER is not needed to create objects from it. It just
serves to express the constraint that the formal generic G has to satisfy the
concept of a total order relation.

Predicate “is_sorted”

We need a predicate which tells whether a list is sorted and whether an array
is sorted.

 is_sorted(l:LIST[G]): ghost BOOLEAN
 ensure
 Result = all(x,y:G) [x,y] in l.tail_zipped => (x<=y)
 end
 is_sorted(a:ABSTRACT_ARRAY[G]): ghost BOOLEAN
 ensure
 Result = a.content.is_sorted
 end

Note that the predicates need not be computable. It is easy to make them
computable. But it is not worth the effort.

If we have two lists “u+e” and “e::v” which are individually sorted the sum
“u+e+v” is sorted as well.

 glueing:
 all(u,v:LIST[G], e:G)
 require
 (u+e).is_sorted
 (e::v).is_sorted
 ensure
 (u+e+v).is_sorted
 end

This claim can be proved by

 all(u,v:LIST[G], e:G)
 require
 r1: (u+e).is_sorted
 r2: (e::v).is_sorted
 check
 all(x,y:G)
 require
 [x,y] in (u+e+v).tail_zipped
 check
 (u+e+v).tail_zipped = (u+e).tail_zipped + (e::v).tail_zipped
 if [x,y] in (u+e).tail_zipped then
 x<=y -- r1
 else
 [x,y] in (e::v).tail_zipped
 x<=y -- r2
 end
 ensure
 x<=y
 end
 ensure
 (u+e+v).is_sorted
 end

The basic algorithm

The procedure “sort” has to satisfy the contract:

 feature
 sort(a:ABSTRACT_ARRAY[G])
 ensure
 a.is_sorted
 a.content.is_permutation(old a.content)
 end
 end

The algorithm needs a loop which keeps some prefix of length “i” of “a”
sorted. I.e. the loop works with the invariant

 i <= a.count
 a.content.take(i).is_sorted
 a.content.is_permutation(old a.content)

The invariant is satisfied if we initialize “i” with zero. At each step of the
algorithm we have to make the sorted prefix of “a” one element larger. The
following algorithm does the job.

 feature
 sort(a:ABSTRACT_ARRAY[G])
 local
 i: NATURAL := 0
 do
 from invariant
 i <= a.count
 a.content.take(i).is_sorted
 a.content.is_permutation(old a.content)
 variant
 a.count - i
 until
 i = a.count
 loop
 insert_ith(a,i) -- see below
 i := i + 1
 end
 ensure
 a.is_sorted
 end
 end

It is easy to verify that after termination of the loop the result is
valid. The exit condition states “i=a.count” and the invariant guarantees
“a.content.take(i).is_sorted”. Both imply the postcondition.

In order to prove the algorithm correct we need to make sure that the
invariant is maintained in each iteration of the loop. In order to prove this
we need the assignment axiom.

 -- Assigment axiom: "x" must be a local variable and
 -- must not be an attribute of the surrounding class!
 all[G](x,exp:G, cond:BOOLEAN)
 require
 cond[x:=exp]
 do
 x := exp
 ensure
 cond
 end

It basically states the following: “If we want to have a boolean condition
“cond” valid after the assignment statement “x:=exp” then we have to guarantee
that “cond[x:=exp]” (i.e. cond with all free occurrences of “x” substituted by
“exp”) is valid before the assignment.

With the assignment axiom we can backtransform the invariant through the
statement “i:=i+1” and get

 require
 r1: i+1 <= a.count
 r2: a.content.take(i).is_sorted
 r3: a.content.is_permutation(old a.content)
 do
 i := i + 1
 ensure
 i <= a.count
 a.content.take(i+1).is_sorted
 a.content.is_permutation(old a.content)
 end

The procedure “insert_ith” cannot modify “i” (NATURAL is immutable). Therefore
the condition “r1” can be derived from the invariant “i<=a.count” and the
negated exit condition “i/=a.count”.

The condition “a.content.take(i+1).is_sorted” must be established by
“insert_ith” and the condition “a.content.is_permutation(old a.content)” must
be maintained.

Therefore the procedure “insert_ith” has to satisfy the contract

 require
 i < a.count -- from the loop invariant and negated exit
 -- condition
 a.content.take(i).is_sorted -- from the loop invariant
 a.content.is_permutation(old a.content) -- from the loop invariant
 do
 insert_ith(a,i)
 ensure
 a.content.take(i+1).is_sorted
 a.content.is_permutation(old a.content)
 end

The procedure “insert_ith”

Contract of “insert_ith”

We need a procedure “insert_ith” which satisfies the contract

 feature{NONE}
 insert_ith(a:ABSTRACT_ARRAY[G], i:NATURAL)
 require
 i < a.count
 a.content.take(i).is_sorted
 ensure
 a.content.take(i+1).is_sorted
 a.content.is_permutation(old a.content)
 end
 end

The procedure can be private, therefore the “feature{NONE}”.

Description of the loop

We need a loop to establish the postcondition, because the element “a[i]” has
to be put in the correct position. We swap it with the previous element as
long as the previous element greater than the element to be inserted. The loop
terminates if the previous element is not greater than the element to be
inserted.

In order to specify the algorithm we need a predicate that a list is sorted
except at one position.

 is_sorted_except(l:LIST[G], j:NATURAL): ghost BOOLEAN
 ensure
 Result = check
 sorted_without_j: (l.take(j)+l.drop(j+1)).is_sorted
 sorted_from_j: l.drop(j).is_sorted
 end
 end

At the enty point of the routine the condition

 a.content.take(i+1).is_sorted_except(i)

is valid because “a.content.take(i).is_sorted” is already valid and
“a.content.take(i+1)” has just one element more (the element “i”). Therfore it
is sorted except at position “i”. Note that “a.content.take(i+1).drop(i+1)” is
empty and “a.content.take(i+1).drop(i)” has just one element.

The algorithm uses a loop with the loop variable “j”. The variable “j” has
initially the value “i”. The loop body decreases the variable “j” at each
iteration maintaining the invariant.

We use the following invariant

 j <= i
 a.content.is_permutation(old a.content)
 a.content.take(i+1).is_sorted_except(j)

and the following pattern for the algorithm:

 insert_ith(a:ABSTRACT_ARRAY[G], i:NATURAL)
 require
 i < a.count
 a.content.take(i).is_sorted
 local
 j:NATURAL := i
 do
 from invariant
 inv1: j <= i
 inv2: a.content.is_permutation(old a.content)
 inv3: a.content.take(i+1).is_sorted_except(j)
 variant
 j
 until
 -- a.content.take(i+1).is_sorted
 loop
 -- establish the invariant for decreased j
 j := j-1
 end
 ensure
 a.content.take(i+1).is_sorted
 a.content.is_permutation(old a.content)
 end

The algorithm is already correct, we just need to fill in the missing parts.

Exit condition

Since we have the invariant “inv3” we know that “a.content.take(i+1).drop(j)”
is always sorted. In case of “j=0” this is identical to “a.content.take(i+1)”
and we can terminate the loop. Therefore “j=0” is one possible exit condition.

But there is a second possibility. The element at the exception position “j”
might fit already well. This is the case if “a[j-1]<=a[j]” is valid. I.e. the
complete exit condition is

 j=0 or a[j-1]<=a[j] -- exit condition

We have to prove that the exit condition and the invariant guarantee the
desired result. The following lemma verifies exactly that condition.

 all(l:LIST[G], j:NATURAL)
 require
 r1: j < l.count
 r2: l.is_sorted_except(j)
 r3: j=0 or l[j-1]<=l[j]
 check
 if j=0 then
 c1: l.drop(0).is_sorted -- r2
 c2: l.is_sorted
 else
 c3: l[j-1] <= l[j] -- r3 and "j/=0"
 c4: (l[j]::l.drop(j+1)).is_sorted -- r3, "sorted_from_j"
 c5: (l[j-1]::l[j]::l.drop(j+1).is_sorted -- c3,c4
 c6: (l.take(j-1)+l[j-1]).is_sorted -- r3, "sorted_without_j"
 c7: (l.take(j-1)+l[j-1]::l[j]::l.drop(j+1)).is_sorted
 -- paste c5,c6
 c8: l.is_sorted -- c7
 end
 ensure
 l.is_sorted -- c2,c8
 end

Establish the invariant for decreased “j”

At the entry point of the loop body the exit condition is invalid (otherwise
the loop would be terminated). The negated exit condition is

 j/=0 and a[j] < a[j-1] -- negated exit condition

i.e. “a[j-1]” and a[j] are out of order. The element a[j] is still to small
for its position. We simply swap the two elements. Since the sequence without
“a[j]” is perfectly sorted, the invariant is kept. Just the possible out of
order element has been pushed one position down.

We get the complete loop

 from invariant
 inv1: j <= i
 inv2: a.content.is_permutation(old a.content)
 inv3: a.content.take(i+1).is_sorted_except(j)
 variant
 j
 until
 j=0 or a[j-1]<=a[j]
 loop
 a.swap(j-1,j)
 j := j-1
 end

The following lemma verifies that the invariant “inv3” is maintained.

 all(l,ls:LIST[G], i,j:NATURAL)
 require
 r1: j /= 0
 r2: j < l.count
 r3: l.is_sorted_except(j)
 r4: l[j]<=l[j-1]
 check
 c01: (l.take(j) + l.drop(j+1)).is_sorted -- r3, def "is_sorted_except"
 c02: l.drop(j).is_sorted -- r3, def "is_sorted_except"
 c03: (l[j]::l.drop(j+1)).is_sorted -- c02
 c04: (l[j-1]::l.drop(j+1)).is_sorted -- c01
 c09: (l.take(j-1) + l[j-1]::l.drop(j+1)).is_sorted -- c01, assoc
 c10: (l[j]::l[j-1]::l.drop(j+1)).is_sorted -- c03,c04,r4
 ensure
 l.swapped(j-1,j).is_sorted_except(j-1)
 -- c09, c10, swap2, swap3, swap4, def "is_sorted_except"
 end
 end

The complete algorithm

 -- module: insertion_sorter
 immutable class
 INSERTION_SORTER[G:ORDER]
 end
 feature
 is_sorted(l:LIST[G]): ghost BOOLEAN
 ensure
 Result = all(x,y:G) [x,y] in l.tail_zipped => (x<=y)
 end
 is_sorted(a:ABSTRACT_ARRAY[G]): ghost BOOLEAN
 ensure
 Result = a.content.is_sorted
 end
 sort(a:ABSTRACT_ARRAY[G])
 local
 i: NATURAL := 0
 do
 from invariant
 i <= a.count
 a.content.take(i).is_sorted
 a.content.is_permutation(old a.content)
 variant
 a.count - i
 until
 i = a.count
 loop
 insert_ith(a,i) -- see below
 i := i + 1
 end
 ensure
 a.is_sorted
 end
 end
 feature {NONE}
 is_sorted_except(l:LIST[G], j:NATURAL): ghost BOOLEAN
 ensure
 Result = check
 sorted_without_j: (l.take(j)+l.drop(j+1)).is_sorted
 sorted_from_j: l.drop(j).is_sorted
 end
 end
 insert_ith(a:ABSTRACT_ARRAY[G], i:NATURAL)
 require
 i < a.count
 a.content.take(i).is_sorted
 local
 j:NATURAL := i
 do
 from invariant
 inv1: j <= i
 inv2: a.content.is_permutation(old a.content)
 inv3: a.content.take(i+1).is_sorted_except(j)
 variant
 j
 until
 j=0 or a[j-1]<=a[j]
 loop
 a.swap(j-1,j)
 j := j-1
 end
 ensure
 a.content.take(i+1).is_sorted
 a.content.is_permutation(old a.content)
 end
 end

Leave a comment Cancel reply