CIS301 Monday, Feb. 17    NAME___sample answer______

A sequence of ints, s, is *ordered* if  s[0] <= s[1] <= ..., etc:

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

Two sequences, s and t, are *permutations of each other* if they have exactly the same values (but maybe ordered differently):

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

def insert(n, s):
    """inserts  n  in the proper place in ordered sequence  s"""
    """{ pre  int n  and  int[] s  and  isOrdered(s)
(!)      post in words:  "ans  contains all of  s's  elements and
                          also  n  so that ans is ordered"

(!)     post in logic:  arePerms(ans, s + [n]) and isOrdered(ans)
                # NOTE: s + [n]  adds  n  to end of list s
        return  ans
    }"""
    i = 0
    while (n > s[i]) :
(!)    """{ invariant in words:     "the first i+1 elements of  s
                                     are all smaller than  n"
(!)         invariant in logic: forall 0 <= j <= i,  n > s[j]
       }"""
       i = i + 1
(!) # GOAL ACHIEVED BY LOOP, in words:  "i  is the position
    #                    within  s  where  n  should be inserted"
    # The Goal stated in logic is 
    #     (forall 0 <= j < i,  s[j] < n) 
    #     and (forall i <= k < len(s), n <= s[k])

    ans = s[:i] + n + s[i:]  // split s and place n at position i
    # NOTE:  s[:i] == [s[0],...,s[i-1]] "all elems up to i"
    #  s[i:] == [s[i],...,s[len(s)-1]]  "all elems from i to end"
    return ans

def insertionSort(s) :
    """conducts insertion sorting on int sequence  s"""
    """{ pre     int[] s
         post    arePerms(s, ans) and isOrdered(ans)
         return  ans
    }"""
    ans = []
    i = 0
    while (i != len(s)) :
(!)    """{ invariant in words: "ans  holds the first i elements
                                 of  s, in sorted order"

(!) invariant in logic:  isOrdered(ans) and arePerms(ans, s[:i])
       }"""
       ans = insert(s[i], ans)
       i = i + 1
    return ans