sort.py 887 Bytes
 Jean-Christophe Filliâtre committed Jan 31, 2017 1 `````` `````` Jean-Christophe Filliâtre committed Jan 31, 2017 2 3 4 5 6 ``````from random import randint n = 42 a = [0] * n `````` Andrei Paskevich committed Feb 01, 2017 7 8 ``````### On remplit le tableau "a" `````` Jean-Christophe Filliâtre committed Jan 31, 2017 9 10 11 ``````for i in range(0, len(a)): a[i] = randint(0, 100) `````` Jean-Christophe Filliâtre committed Jan 31, 2017 12 13 ``````print(a) `````` Andrei Paskevich committed Feb 01, 2017 14 15 ``````### Et maintenant on le trie `````` Jean-Christophe Filliâtre committed Jan 31, 2017 16 17 ``````m = 1 while m < len(a): `````` Jean-Christophe Filliâtre committed Jan 31, 2017 18 `````` #@ invariant 1 <= m <= len(a) `````` Jean-Christophe Filliâtre committed Jan 31, 2017 19 `````` #@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j] `````` Jean-Christophe Filliâtre committed Jan 31, 2017 20 `````` #@ variant len(a) - m `````` Jean-Christophe Filliâtre committed Jan 31, 2017 21 22 23 24 `````` x = a[m] k = m while k > 0 and a[k-1] > x: #@ invariant 0 <= k <= m `````` Jean-Christophe Filliâtre committed Jan 31, 2017 25 26 27 `````` #@ 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] #@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j] `````` Andrei Paskevich committed Feb 01, 2017 28 `````` #@ invariant forall j. k < j <= m -> x < a[j] `````` Jean-Christophe Filliâtre committed Jan 31, 2017 29 `````` #@ variant k `````` Jean-Christophe Filliâtre committed Jan 31, 2017 30 31 32 33 34 35 36 `````` 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] `````` Jean-Christophe Filliâtre committed Jan 31, 2017 37 ``````print(a) `````` Jean-Christophe Filliâtre committed Jan 31, 2017 38