mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
16 lines
559 B
Python
16 lines
559 B
Python
|
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]
|