forked from epfl-lara/stainless
-
Notifications
You must be signed in to change notification settings - Fork 0
/
InnerFunctions.scala
65 lines (58 loc) · 1.24 KB
/
InnerFunctions.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
// Testing FunctionClosure captures for PC variables
object InnerFunctions {
def outer1(x: BigInt): Unit = {
require(x >= 0)
def inner1(): Unit = ()
}
def outer2(x: BigInt): Unit = {
val y = x
val z = y
def inner2(a: BigInt): Unit = ()
}
def outer3(x: BigInt, a: BigInt): Unit = {
require(x >= 0 && a >= x)
def inner3(y: BigInt): Unit = {
val b = a
assert(a >= 0)
assert(b >= 0)
}
}
def outer4(x: BigInt): Unit = {
require(x >= 0)
val a = x - 2
def inner4(y: BigInt): Unit = {
val b = a
assert(a >= -2)
assert(b >= -2)
}
}
def outer5(x: BigInt, y: BigInt, z: BigInt) = {
require(0 <= x && x <= y)
require(z >= 42)
val a = x + 1
def inner5A = {
val aa = a + 1
assert(aa >= 2)
}
def inner5B = {
val yy = y
assert(yy >= 0)
}
}
def outer6(x: BigInt, y: BigInt, z: BigInt) = {
require(0 <= x && x <= y)
require(z >= 42)
val a = x + 1
def inner6A = { val aa = a + 1 }
def inner6B = { val yy = y }
}
def outer7(x: BigInt): Unit = {
require(0 < x && x < 10)
val y = x
val z = y + 10
def inner7(w: BigInt): Unit = {
require(w < z)
assert(w < 20)
}
}
}