File: selection_sort.py

package info (click to toggle)
why3 1.8.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 45,028 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (15 lines) | stat: -rw-r--r-- 559 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
def tri_selection(L):
    #@ ensures forall i. forall j. 0<=i<j<len(L) -> L[i]<=L[j]
    im = 0
    for i in range(len(L)):
        #@ invariant forall k. forall l. 0<=k<i<=l<len(L) -> L[k]<=L[l]
        #@ invariant forall k. forall l. 0<=k<=l<i -> L[k]<=L[l]
        im = i
        for j in range(i+1,len(L)):
            #@ invariant i<=im<j
            #@ invariant forall k. i<=k<j -> L[im]<=L[k]
            if L[j]<L[im]:
                im = j
        if im != i:
            L[im], L[i] = L[i], L[im]
        #@ assert forall k. 0<=k<i -> L[k]<=L[i]