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