#!/usr/bin/python

## Assume A0 is the initial value of the array A[0..n-1]
## ordered (A, p, q) = forall j: 0 <= p <= j < q < n -> A[j] <= A[j+1]
## leftmin (A, p ) = forall i: 0 <= i < p < n: forall j: p <= j< n: A[i] <= A[j]

## INV: perm (A, A0) /\ 0 <= p < n /\ ordered (A, p, n-1) /\ rightmax (A, p)

def swap (A, i, j):
    s = len (A)
    if (i in range(s)) and (j in range(s)): 
        t = A[i]
        A[i] = A[j]
        A[j] = t
    else:
        raise NameError('Array index out of bounds')

def selectionSort (A):
    
    def findIndexOfMin (A, i, n): # assume 0 <= r < n
        m = i
        k = i
        # INV2: 0<= i <= m <= k  /\ for all j: 0 <= i<=j < k <= n: A[m] <= A[j] 
        while k < n:
            if A[k] < A[m]:
                m = k
            k = k+1
        return m
    # findIndexOfMin (A, i, n) ends
    
    # body of selectionSort begins
    n = len(A)
    p = 0
    q = 0
    # INV1: perm (A, A0) /\ 0 <= p <= n /\ ordered (A, 0, p) /\ leftmin (A, p)
    while p < n:
        q = findIndexOfMin (A, p, n)
        swap (A, q, p)
        p = p+1
# selectionSort ends
# try it 
A = [10, 23, 21, 45, -12, -10, 67, 98]
print A
selectionSort (A)
print A
