examples/python/is_sorted.py

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):
        #@ invariant forall j1,j2. 0 <= j1 <= j2 <= i -> l[j1] <= l[j2]
        if l[i+1] < l[i]:
            return False
    return True

a = [2, 3, 4]
a.sort()
c = is_sorted(a)

#@ assert c
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`