{true}
{A[0] = A[0] & 0=0}
m = A[0]
{m = A[0] & 0=0 & m is contained in the array}
i = 0
{m = A[0] & i=0& m is contained in the array}
{for all k<=i m<=A[k] &i=0& m is contained in the array}
do
 {for all k<=i m<=A[k] &i=0 v for all k < i m<=A[k] & i <=n& m is contained in the array}
 {for all k<i m<=A[k] & i <= n& m is contained in the array}
until i = n
 {for all k<i m<=A[k] & i<=n & i!=n& m is contained in the array}
 {for all k<i m<=A[k] & i < n& m is contained in the array}
 if m > A[i]
  {for all k<i m<=A[k] & m>A[i] & i < n& m is contained in the array}
  {for all k<=i A[i] <= A[k] & i < n& A[i] is contained in the array}
  m = A[i]
  {for all k<=i m <= A[k] & i < n & m is contained in the array}
 else
  {for all k<i m<=A[k] & m<=A[i] & i < n & m is contained in the array}
  {for all k<=i m<=A[k]& i < n & m is contained in the array}
 end if
 {for all k<=i m<=A[k]& i < n & m is contained in the array}
 {for all k<i+1 m<=A[k] & i+1 <=n& m is contained in the array}
 i = i+1
 {for all k < i m<=A[k] & i <=n& m is contained in the array}
end do
{for all k < i m<=A[k] & i <=n & i=n& m is contained in the array}
{for all k < i m<=A[k] & i=n& m is contained in the array}
{for all k < n m<=A[k]& m is contained in the array}

I know that m <= everything in the array.  But I never proved that m is itself somewhere in the array.

for some k<n m = A[k]

m = A[0]
i = 0
do
until i = n
 if m > A[i]
  m = A[i]
 else
 end if
 i = i+1
end do

The above formal verification proves that our algorithm is partially correct.  "Correct provided it terminates."

How do we prove that the loop terminates?

The technique I use is based on Well-Ordering Principle of Cardinal numbers.  "Any nonempty set of cardinal numbers has a smallest member."

The corollary is that if you start from ANY cardinal number and repeatedly choose a smaller number from what you have already chosen, you will choose zero after a FINITE number of steps.

If we have an integer flag that always gets smaller and never goes negative, the loop must terminate.  (You will get to zero in a finite number of steps.)  (And...if you have to...you can initialize the flag to be a cardinal infinity, and the idea still works.)

{true}
{A[0] = A[0] & 0=0}
m = A[0]
{m = A[0] & 0=0 & m is contained in the array}
i = 0
{m = A[0] & i=0& m is contained in the array}
{for all k<=i m<=A[k] &i=0& m is contained in the array & n=n}
ct = n
{for all k<=i m<=A[k] &i=0& m is contained in the array & ct=n & ct>=0 & n+1=n+1}
oct = n+1
{for all k<=i m<=A[k] &i=0& m is contained in the array & ct=n-i & ct>=0 & oct=n+1}
{for all k<=i m<=A[k] &i=0& m is contained in the array & ct=n-i & ct>=0 & ct < oct}
do
 {for all k<=i m<=A[k] &i=0 v for all k < i m<=A[k] & i <=n& m is contained in the array & ct=n-i & ct>=0 & ct < oct}
 {for all k<i m<=A[k] & i <= n& m is contained in the array  & ct=n-i & ct>=0 & ct < oct}}
until i = n
 {for all k<i m<=A[k] & i<=n & i!=n& m is contained in the array& ct=n-i & ct>=0 & ct < oct}}
 {for all k<i m<=A[k] & i < n& m is contained in the array& ct=n-i & ct>=0 & ct < oct}}
 if m > A[i]
  {for all k<i m<=A[k] & m>A[i] & i < n& m is contained in the array& ct=n-i & ct>=0 & ct < oct}}
  {for all k<=i A[i] <= A[k] & i < n& A[i] is contained in the array& ct=n-i & ct>=0 & ct < oct}}
  m = A[i]
  {for all k<=i m <= A[k] & i < n & m is contained in the array& ct>=0 & ct < oct}}
 else
  {for all k<i m<=A[k] & m<=A[i] & i < n & m is contained in the array& ct=n-i & ct>=0 & ct < oct}}
  {for all k<=i m<=A[k]& i < n & m is contained in the array& ct=n-i & ct>=0 & ct < oct}
 end if
 {for all k<=i m<=A[k]& i < n & m is contained in the array& ct=n-i & ct>=0 & ct < oct}
 {for all k<i+1 m<=A[k] & i+1 <=n& m is contained in the array& ct=n-i & ct>=0 & ct < oct}
 {for all k<i+1 m<=A[k] & i+1 <=n& m is contained in the array& ct=n-(i+1)+1 & ct>=0 & ct < oct}
 i = i+1
 {for all k < i m<=A[k] & i <=n& m is contained in the array& ct = n-i+1 & ct>=0 & ct < oct}
 {for all k < i m<=A[k] & i <=n& m is contained in the array& ct >= 0 & ct = n-i+1 & oct > 0}
 {for all k < i m<=A[k] & i <=n& m is contained in the array& ct > 0 & ct = n-i+1 & ct=ct}
 oct = ct
 {for all k  < i m<=A[k] & i <=n& m is contained in the array& ct = n-i+1 & oct>0 & oct=ct}
 {for all k  < i m<=A[k] & i <=n& m is contained in the array& ct-1 = n-i & oct>0 & oct-1=ct-1}
 ct = ct-1
 {for all k  < i m<=A[k] & i <=n& m is contained in the array& ct = n-i & oct>0 & oct-1=ct & ct < oct & ct >=0}
end do
{for all k < i m<=A[k] & i <=n & i=n& m is contained in the array & ct=n-i & ct>=0 & ct < oct}
{for all k < i m<=A[k] & i=n& m is contained in the array}
{for all k < n m<=A[k]& m is contained in the array}

Any time we complete a cycle, ct >=0 and ct < oct.  Since oct is defined the previous value of ct (in fact, we set oct to ct in line 91), we see ct strictly decreases with every cycle and never falls below zero.

The loop must then terminate at some point.

Total correctness:  add two variables (ct, oct).  Before you update ct, set oct = ct.  Prove that ct is always < oct and always >= 0, and you have proven that the loop terminates.

i = 0
do
{i>=0 & the last i elements are in sorted order and everything in the array before the last i elements are <= the last i elements}
{for all k such that n-i < k < n-1  A[k] <= A[k+1] &
 for k <= n-i  A[k] <= A[n-i] (unless i=0)
until i=n
 j = 0
 do
 {i>=0 & the last i elements are in sorted order and everything in the array before the last i elements are <= the last i elements &
  for all k < j,  A[k] <= A[j] (or all elements before position j in
  the array are <= A[k]).
 until j=n-1
  if A[j] > A[j+1]
{ for k < j A[k] <= A[j] & A[j] > A[j+1]
   t = A[j]
{for k < j  A[k] <= t & t > A[j+1]
   A[j] = A[j+1]
{for k < j   A[k] <= t & t > A[j]
   A[j+1] = t
{for k < j  A[k] <= A[j+1] & A[j+1] > A[j]}
{for k < j+1  A[k] <= A[j+1]
  else
{for k < j A[k] <= A[j] & A[j] <= A[j+1]}
{for k < j+1 A[k] <= A[j+1]}
  end if
{for k < j+1 A[k] <= A[j+1]}
  j = j+1
{for k < j A[k] <= A[j]
 end do
 i = i+1
end do




4 8 9 5 5

Shell Sort  (Math Sort)

Q W E R T Y U I O P

10:9,8,6,4,3,2,


Compare and swap items that are 9 apart
Q W E R T Y U I O P

P W E R T Y U I O Q

Compare and swap items that are 8 apart

P W E R T Y U I O Q

O W E R T Y U I P Q

O Q E R T Y U I P W

Compare and swap items that are 6 apart

O I E R T Y U Q P W

Compare and swap items that are 4 apart

O I E Q T Y U R P W

O I E Q P Y U R T W

O I E Q P W U R T Y

Compare and swap items that are 3 apart

O I E Q P T U R W Y

Compare and swap items that are 2 apart

E I O Q P T U R W Y

E I O Q P R U T W Y

Compare and swap items that are 1 apart

E I O P Q R U T W Y

E I O P Q R T U W Y

The reason this works is that in any pass, no element ever has to be swapped more than once.  Why?  Because our passes only involve prime factors of only 2 and 3 and you use number theory to prove that you don't have to swap anything more than once.

100: 96,84,81,72,64,54,48,36,32,27,24,18,16,12,9,8,6,4,3,2,1

For a list of size n, there are about lg^2 n numbers with only 2 and 3 as prime factors.  Each takes THETA(n) time, so Shell Sort runs in
THETA (n lg^2 n) time.  Faster than Bubble Sort, slower than Quick Sort.

Requires no recursion, and no auxiliary array, just a small number of local variables, and the code is short.

But because no element is swapped twice during any pass, it does not matter what order you swap things in, which means this sorting algorithms parallelizes very nicely.  With parallelization, this runs in THETA (lg^2 n) time, which USED TO BE THOUGHT to be the minimum for parallel sorting.


W O N D E R W O M A N

W0 O1 N2 D3 E4 R5 W6 O7 M8 A9 N10