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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
module A {
const i: int := 56_78
}
method m(b: bool, s: string) {
var x: string;
var i: int;
assert b;
}
function f(i: int): int { i + 1 }
// comment
// comment /* not a nested comment
/* comment
// nested comment
more comment
*/
/* nested /* comment */ more comment */
/* bad nested // comment */
more bad comment
*/
/* bad nested " comment */a xyz //"
more bad comment
*/
const i: int := 123_456
const i: int := _123_456 // Error
const i: int := 123_456_ // Error
const i: int := 123abc // Error
const h: int := 0x0123456789_abcdef_ABCDEF
const h: int := 0x0123456789_abcdef_ABCDEF_ // Error
const b: int := 0b0101_0101_010
const b: int := 0b0101_0101_010_ // Error
const b: int := 0bZ0101 // Error
const b: int := 0b010145 // Tail is not bin
const h: int := 0xabcXYZa // Tail is not hex
const h: int := 0xZ4545 // Error
const b: int := 0b
const h: int := 0x
const c: char := 'z'
const c: char := '"'
const c: char := '\0'
const c: char := '\\'
const c: char := ' '
const c: char := '\Z' // Error
const c: char := 'a\' // Error
const c: char := 'a // Error
const c: char := 'a // Error
const c: char := '\z // Error
const c: char := '' // Error - and the next line, which ends with a '
const c: char := '
const s: string := "asd\"\'\\\n\r\t"
const s: string := "Z\u1234Z"
const s: string := ""
const s: string := "asd\"\'\\\n\r\txyz // Error -- next line also
const s: string := "
const s: string := "\z" // Error -- bad escape -- next 2 lines also
const s: string := "\t
const s: string := "\z
const ss: string := @"asd ' "
const ss: string := @"asd '"" xyz
XYZ "
// Operators
+ - * / % ! << >> ==> <== <==> & | ^ && || != == := :-
< > <= >= . .. =
// Punctuation
( ) [ ] { } , ; `
5..6
5 as nat
7 is nat
// Errors?
# @ ~ __
// Identifiers
abc def_ ghi? klm'pqr
A9090 _
setxxx set000 ifxxx asxx isxx truexxx true000
set_ if_ as_ is_ int_ true_
set' if' as' is' int' true'
// Types
bool char int real string object object?
seq set map iset imap multiset
array array2 array10 array? array2? array10?
bv0 bv1 bv10 bv9
// Ids
array1 array1? arrayxx array?xx array2xx array2?xxx
// Constants
false true null
// Text Operators
as is in !in
// Keywords
abstract assert assume
break calc case class codatatype constructor
datatype decreases default
else ensures exists expect extends
forall fresh function
ghost greatest if import include
inductive invariant
iterator label least lemma match method
modifies modify module
new newtype old opened
predicate print provides reads
refines requires return returns reveals
static
then this trait twostate type
unchanged var where while yield yields
// At end of file
const ss: string := @"unclosed verbatim string
more
|
