Logo
Explore Help
Sign In
ada/why3
0
0
Fork 0
You've already forked why3
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples/python/is_sorted.py

14 lines
323 B
Python
Raw Permalink Normal View History

Python: Added examples - New examples using the new syntax (+=, ...) - New examples using the new methods (.pop(), .append(), ...) - Update old examples with assignement operators (+=, ...)
2021-06-23 17:45:21 +02:00
def is_sorted(l):
#@ ensures result == (forall j1,j2. 0 <= j1 <= j2 < len(l) -> l[j1] <= l[j2])
for i in range(len(l)-1):
fixed Python example and proof session
2022-09-09 14:56:11 +02:00
#@ invariant forall j1,j2. 0 <= j1 <= j2 <= i -> l[j1] <= l[j2]
Python: Added examples - New examples using the new syntax (+=, ...) - New examples using the new methods (.pop(), .append(), ...) - Update old examples with assignement operators (+=, ...)
2021-06-23 17:45:21 +02:00
if l[i+1] < l[i]:
return False
return True
fixed Python example and proof session
2022-09-09 14:56:11 +02:00
a = [2, 3, 4]
Python: Added examples - New examples using the new syntax (+=, ...) - New examples using the new methods (.pop(), .append(), ...) - Update old examples with assignement operators (+=, ...)
2021-06-23 17:45:21 +02:00
a.sort()
c = is_sorted(a)
#@ assert c
Reference in New Issue Copy Permalink
Powered by Gitea Page: 228ms Template: 14ms
English
English
Licenses API