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