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
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
```