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