Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
bd52075c
Commit
bd52075c
authored
Jan 31, 2017
by
Jean-Christophe Filliâtre
Browse files
ascii art
parent
de593c35
Changes
1
Hide whitespace changes
Inline
Side-by-side
plugins/python/examples/sort.py
View file @
bd52075c
from
random
import
randint
n
=
42
...
...
@@ -17,10 +18,10 @@ while m < len(a):
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]
#@ 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]
#@ invariant forall j.
k <
j <= m ->
x
<
a[j]
#@ variant k
a
[
k
]
=
a
[
k
-
1
]
k
=
k
-
1
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment