sort.py 826 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
from random import randint

n = 42
a = [0] * n

for i in range(0, len(a)):
    a[i] = randint(0, 100)
    print(a[i])

#for m in range(1, len(a)):
m = 1
while m < len(a):
    #@ invariant 0 <= m <= len(a)
    #@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j]
    #@ variant len(a) - m
    x = a[m]
    k = m
    while k > 0 and a[k-1] > x:
        #@ invariant 0 <= k <= m
        #@ invariant forall j. k < j <= m -> x < a[j]
        #@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j]
        #@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j]
        #@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j]
        #@ variant k
        a[k] = a[k-1]
        k = k - 1
    a[k] = x
    m = m + 1

#@ assert forall i,j. 0 <= i <= j < len(a) -> a[i] <= a[j]

for i in range(0, len(a)):
    print(a[i])