blob: b53b1ca853a914967005f8b97da5b543a037422d (
plain)
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
Make integer safety opt-in?
===========================
Integer safety should be:
* Opt-in at the function declaration, and
* Part of API, and
* Backwards-compatible with unsafe declarations
(unsafe callers will just assert-fail/trap if the value is out of range)
There's still the problem of multi-variable checks, e.g. `a+b<100`.
Maybe that should simply not be supported, and instead be written as
either `a<50, b<50`, or `a<100, b<100` together with an assert.
Syntax test
-----------
Note that `int` in SLUL is non-negative!
(`signed int` allows negative values.)
Syntax 1:
func calc
int x
int y
int q
require
1 <= x <= 100
1 <= y <= 100
q <> 0
...
Syntax 2:
func calc
int x in 1..=100
int y in 1..=100
int q not 0
...
Syntax 3:
func calc
int x from 1 to 100
int y from 1 to 100
int q not 0
...
Syntax 4:
func calc
int x min 1 max 100
int y min 1 max 100
int q not 0
...
Scope
-----
In scope:
* Basic range checking + forbidden values/range.
(note that exclusions could be implemented as a disjoint range)
* A single lower bound that's tied to (immutable_variable+constant).
* A single upper bound that's tied to (immutable_variable+constant).
This is useful for lengths of lists/arrays etc.
Not in scope / Won't be supported:
* Complex expressions.
* Boolean expressions.
* Mutable ranges.
* Multi-level dependencies in bounds, e.g. `a<10`, `b<a`, `c<b`
Integer safety in the bootstrap compiler?
-----------------------------------------
Options:
* Best-effort. Reject complex cases.
* Best-effort. Emit warning in complex cases.
* Best-effort. Disable checks in complex cases.
* No checks at all.
|
