mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
3671864507
- New examples using the new syntax (+=, ...) - New examples using the new methods (.pop(), .append(), ...) - Update old examples with assignement operators (+=, ...)
18 lines
520 B
Python
18 lines
520 B
Python
def reverse(a):
|
|
#@ requires len(a) > 0
|
|
#@ ensures len(result) == len(old(a))
|
|
#@ ensures len(a) == 0
|
|
#@ ensures forall i. 0 <= i < len(result) -> result[i] == (old(a))[-(i+1)]
|
|
#@ label L
|
|
|
|
res = []
|
|
|
|
while(len(a) != 0):
|
|
#@ invariant len(a) + len(res) == at(len(a), L)
|
|
#@ invariant forall i. 0 <= i < len(res) -> res[i] == at(a[-(i+1)], L)
|
|
#@ invariant forall i. 0 <= i < len(a) -> a[i] == at(a[i], L)
|
|
#@ variant len(a)
|
|
res.append(a.pop())
|
|
|
|
return res
|