python: a slight change in sort

parent 645747d4
......@@ -11,9 +11,9 @@ print(a)
m = 1
while m < len(a):
#@ invariant 0 <= m <= len(a)
#@ invariant 1 <= m <= len(a)
#@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j]
#@ variant len(a) - m
#@ variant len(a) - m
x = a[m]
k = m
while k > 0 and a[k-1] > x:
......@@ -22,7 +22,7 @@ while m < len(a):
#@ 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]
#@ invariant forall j. k < j <= m -> x < a[j]
#@ variant k
#@ variant k
a[k] = a[k-1]
k = k - 1
a[k] = x
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment