tests/sort++.py

   1
   2 from random import randint
   3
   4 n = 42
   5 a = [0] * n
   6
   7 ### On remplit le tableau "a"
   8
   9 for i in range(0, len(a)):
  10     a[i] = randint(0, 100)
  11
  12 print(a)
  13
  14 ### On prend une photo de "a"
  15
  16 photo = [0] * n
  17 k = 0
  18 while k < len(a):
  19     #@ invariant 0 <= k <= len(a)
  20     #@ invariant forall i. 0 <= i < k -> photo[i] == a[i]
  21     #@ variant len(a) - k
  22     photo[k] = a[k]
  23     k = k + 1
  24
  25 #@ assert forall i. 0 <= i < len(a) -> photo[i] == a[i]
  26
  27 ### Et maintenant on le trie
  28
  29 m = 1
  30 while m < len(a):
  31     #@ invariant 1 <= m <= len(a)
  32     #@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j]
  33     #@ invariant forall v. occurrence(v, a) == occurrence(v, photo)
  34     #@ variant   len(a) - m
  35     x = a[m]
  36     k = m
  37     while k > 0 and a[k-1] > x:
  38         #@ invariant 0 <= k <= m
  39         #@ invariant forall i,j. 0 <= i <= j < k               -> a[i] <= a[j]
  40         #@ invariant forall i,j. 0 <= i      < k <      j <= m -> a[i] <= a[j]
  41         #@ invariant forall i,j.               k < i <= j <= m -> a[i] <= a[j]
  42         #@ invariant forall   j.               k <      j <= m -> x    <  a[j]
  43         #@ invariant forall v. occurrence(v, a[k <- x]) == occurrence(v, photo)
  44         #@ variant   k
  45         a[k] = a[k-1]
  46         k = k - 1
  47         #@ assert occurrence(x, a[k <- x]) == occurrence(x, photo)
  48     a[k] = x
  49     m = m + 1
  50
  51 #@ assert forall i,j. 0 <= i <= j < len(a) -> a[i] <= a[j]
  52 #@ assert forall v. occurrence(v, a) == occurrence(v, photo)
  53
  54 print(a)
  55