1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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
|
