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 (+=, ...)
22 lines
624 B
Python
22 lines
624 B
Python
def concat(l1, l2):
|
|
#@ ensures len(result) == len(l1) + len(l2)
|
|
#@ ensures forall i. 0 <= i < len(l1) -> result[i] == l1[i]
|
|
#@ ensures forall i. 0 <= i < len(l2) -> result[len(l1) + i] == l2[i]
|
|
|
|
size1 = len(l1)
|
|
size2 = len(l2)
|
|
size = size1 + size2
|
|
|
|
res = [-1] * size
|
|
|
|
for i in range(size1):
|
|
#@ invariant forall j. 0 <= j < i -> res[j] == l1[j]
|
|
res[i] = l1[i]
|
|
|
|
for i in range(size2):
|
|
#@ invariant forall j. 0 <= j < i -> res[len(l1) + j] == l2[j]
|
|
#@ invariant forall j. 0 <= j < len(l1) -> res[j] == l1[j]
|
|
res[size1 + i] = l2[i]
|
|
|
|
return res
|