CIS301 Weds, Feb. 19    NAME___________________________________

isOrdered(s) ==  forall 0 < i < len(s),  s[i-1] <= s[i]

arePerms(s, t) ==  (len(s) == len(t)) and
               forall 0 <= i < len(s),  s[i] in t  and  t[i] in s


def findIndexOfLeast(s):
    """{ pre  int[] s  and  s != []
(!)      post in words: "least is the index of the smallest int in  s"

(!)      post in logic:  forall 0 <= j < len(s), s[least] <= s[j]

                  OR, say it like this:  forall n in s,  s[least] <= n

         return  least
    }"""
    i = 0
    least = 0
    while (i != len(s)) :
(!)    """{ invariant in words: "least is the index of the smallest int 
                                 in the first  i  elements of  s"

(!)         invariant in logic:  forall 0 <= j < i, s[least] == s[j]

               OR, say it like this:  forall n in s[:i],  s[least] <= n
       }"""
       if s[i] < s[least]:
           least = i
       i = i + 1
(!) # GOAL ACHIEVED BY LOOP, in words: (the same as the postcondition, above)
    #
    return least


def selectionSort(s) :
    """{ pre     int[] s
         post    arePerms(s, ans) and isOrdered(ans)
         return  ans
    }"""
    ans = []
    rest = s   # rest will behave like a duplicate copy of  s
    i = 0
    while (i != len(s)) :
(!)    """{ invariant in words: "ans  holds the smallest i ints in  s, in order"

(!)         invariant in logic (This one is a little harder):
               arePerms(s, rest + ans)  and  isOrdered(ans)  and
               forall 0 <= j < len(rest),  rest[j] >= ans[len(ans) - 1]

            OR, say the second line like this:
               forall m in ans, forall n in rest,  m <= n
       }"""
       leastIndex = findIndexOfLeast(rest)
       ans = ans + [ rest[leastIndex] ]
       rest = rest[:leastIndex] + rest[leastIndex:]  
              # remove the element at leastIndex  from  rest
       i = i + 1
    return ans