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