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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
<Keyword>import </Keyword><String>"foo.tdf"</String><br/>
<Keyword>import </Keyword><String>"foo.txt"</String><br/>
<Keyword>import </Keyword><String>"foo.txt"</String><br/>
<Normal></Normal><br/>
<Keyword>domain</Keyword><Normal> </Normal><Declaration>Foo[T]</Declaration><Normal> </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>axiom</Keyword><Normal> </Normal><Declaration>named</Declaration><Normal> </Normal><Operator>{</Operator><Normal> </Normal><Keyword>forall</Keyword><Normal> x: </Normal><DataType>Int</DataType><Normal>:: </Normal><TriggerZone>{</TriggerZone><Italic>lookup(x)</Italic><TriggerZone>}</TriggerZone><Normal> len(lookup(x)) == foobar(x) </Normal><Operator>}</Operator><br/>
<Normal> </Normal><Keyword>axiom</Keyword><Normal> </Normal><Operator>{</Operator><Normal> </Normal><Keyword>forall</Keyword><Normal> x: </Normal><DataType>Int</DataType><Normal> :: </Normal><TriggerZone>{</TriggerZone><Italic>lookup(x)</Italic><TriggerZone>}</TriggerZone><Normal> </Normal><TriggerZone>{</TriggerZone><Italic>len(lookup(x))</Italic><TriggerZone>}</TriggerZone><Normal> len(lookup(x)) == foobar(x) </Normal><Operator>}</Operator><Normal> </Normal><Comment>// anonymous</Comment><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Comment>// this is a comment</Comment><br/>
<Normal></Normal><br/>
<Comment>/* This is also</Comment><br/>
<Comment> * another multi-line comment</Comment><br/>
<Comment> * With a string "string" and</Comment><br/>
<Comment> * an import "foo.bar" inside */</Comment><br/>
<Normal></Normal><br/>
<Comment>// Any copyright is dedicated to the Public Domain.</Comment><br/>
<Comment>// http://creativecommons.org/publicdomain/zero/1.0/</Comment><br/>
<Normal></Normal><br/>
<Keyword>import </Keyword><String>"empty.sil"</String><br/>
<Normal></Normal><br/>
<Keyword>method</Keyword><Normal> </Normal><Declaration>test1</Declaration><Normal>(xs: </Normal><DataType>Seq</DataType><Normal>[</Normal><DataType>Ref</DataType><Normal>]) </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>inhale</Keyword><Normal> </Normal><Keyword>forall</Keyword><Normal> i: </Normal><DataType>Int</DataType><Normal> :: 0 <= i && i < |xs| ==> xs[i]</Normal><Field>.f</Field><Normal> != </Normal><DecVal>0</DecVal><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Keyword>function</Keyword><Normal> </Normal><Declaration>$</Declaration><Normal>(n: </Normal><DataType>Ref</DataType><Normal>, m: </Normal><DataType>Ref</DataType><Normal>): Node</Normal><br/>
<Normal></Normal><br/>
<Keyword>domain</Keyword><Normal> </Normal><Declaration>Foo[T]</Declaration><Normal> </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>function</Keyword><Normal> </Normal><Declaration>enc</Declaration><Normal>(arg: T): Foo[T]</Normal><br/>
<Normal> </Normal><Keyword>function</Keyword><Normal> </Normal><Declaration>dec</Declaration><Normal>(arg: Foo[T]): T</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>axiom</Keyword><Normal> </Normal><Declaration>ax_Dec</Declaration><Normal> </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>forall</Keyword><Normal> arg: T ::</Normal><br/>
<Normal> dec( enc(arg) ) == arg</Normal><br/>
<Normal> </Normal><Operator>}</Operator><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>axiom</Keyword><Normal> </Normal><Declaration>ax_Enc</Declaration><Normal> </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>forall</Keyword><Normal> arg: Foo[T] ::</Normal><br/>
<Normal> </Normal><TriggerZone>{</TriggerZone><Normal> </Normal><Italic>enc(</Italic><Normal> </Normal><Italic>dec(arg)</Italic><Normal> </Normal><Italic>),</Italic><Normal> </Normal><Italic>foo(bar,</Italic><Normal> </Normal><Italic>i)</Italic><Normal> </Normal><TriggerZone>}</TriggerZone><br/>
<Normal> </Normal><TriggerZone>{</TriggerZone><Normal> </Normal><Italic>dec(arg)</Italic><Normal> </Normal><TriggerZone>}</TriggerZone><br/>
<Normal> enc( dec(arg) ) == arg</Normal><br/>
<Normal> </Normal><Operator>}</Operator><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Keyword>function</Keyword><Normal> </Normal><Declaration>myFunc</Declaration><Normal>(arg: </Normal><DataType>Int</DataType><Normal>): </Normal><DataType>Int</DataType><br/>
<Normal> </Normal><Keyword>requires</Keyword><Normal> </Normal><Constant>true</Constant><Normal> || </Normal><Constant>false</Constant><br/>
<Normal> </Normal><Keyword>ensures</Keyword><Normal> arg <= </Normal><DecVal>0</DecVal><Normal> ==> </Normal><Keyword>result</Keyword><Normal> == -</Normal><DecVal>1</DecVal><br/>
<Normal> </Normal><Keyword>ensures</Keyword><Normal> arg > </Normal><DecVal>0</DecVal><Normal> ==> </Normal><Keyword>result</Keyword><Normal> == arg</Normal><br/>
<Operator>{</Operator><br/>
<Normal> arg > </Normal><DecVal>0</DecVal><Normal> ? arg : myFunc(arg - </Normal><DecVal>1</DecVal><Normal>)</Normal><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Keyword>field</Keyword><Normal> </Normal><Declaration>value</Declaration><Normal>: </Normal><DataType>Int</DataType><br/>
<Keyword>field</Keyword><Normal> </Normal><Declaration>next</Declaration><Normal>: </Normal><DataType>Ref</DataType><br/>
<Normal></Normal><br/>
<Keyword>predicate</Keyword><Normal> </Normal><Declaration>list</Declaration><Normal>(xs: </Normal><DataType>Ref</DataType><Normal>) </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>acc</Keyword><Normal>(xs</Normal><Field>.value</Field><Normal>) && </Normal><Keyword>acc</Keyword><Normal>(xs</Normal><Field>.next</Field><Normal>)</Normal><br/>
<Normal> && ( list(xs</Normal><Field>.next</Field><Normal>) )</Normal><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Keyword>define</Keyword><Normal> </Normal><Declaration>myPureMacro</Declaration><Normal>(abc) abc</Normal><br/>
<Normal></Normal><br/>
<Keyword>define</Keyword><Normal> </Normal><Declaration>myStmtMacro</Declaration><Normal>(abc) </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>inhale</Keyword><Normal> abc</Normal><br/>
<Normal> </Normal><Keyword>exhale</Keyword><Normal> abc</Normal><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Keyword>method</Keyword><Normal> </Normal><Declaration>smokeTest</Declaration><Normal>() </Normal><Operator>{</Operator><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>inhale</Keyword><Normal> </Normal><Constant>false</Constant><Normal>; </Normal><Keyword>exhale</Keyword><Normal> </Normal><Constant>false</Constant><br/>
<Normal> </Normal><Keyword>assume</Keyword><Normal> </Normal><Constant>false</Constant><Normal>; </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>false</Constant><br/>
<Normal></Normal><br/>
<Normal> </Normal><Comment>//magic wands</Comment><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> s: </Normal><DataType>Set</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>]</Normal><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> s </Normal><Operator>setminus</Operator><Normal> s != s</Normal><br/>
<Normal></Normal><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Comment>//:: special comment</Comment><br/>
<Comment>/*</Comment><br/>
<Comment> gfdgfd</Comment><br/>
<Comment>*/</Comment><br/>
<Normal></Normal><br/>
<Keyword>method</Keyword><Normal> </Normal><Declaration>testHighlights</Declaration><Normal>() </Normal><Keyword>returns</Keyword><Normal> ( res: </Normal><DataType>Set</DataType><Normal>[</Normal><DataType>Seq</DataType><Normal>[</Normal><DataType>Multiset</DataType><Normal>[Foo[</Normal><DataType>Int</DataType><Normal>]]]] )</Normal><br/>
<Normal> </Normal><Keyword>requires</Keyword><Normal> </Normal><Constant>true</Constant><br/>
<Normal> </Normal><Keyword>ensures</Keyword><Normal> </Normal><Constant>false</Constant><br/>
<Operator>{</Operator><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> a: </Normal><DataType>Int</DataType><Normal>; </Normal><Keyword>var</Keyword><Normal> b: </Normal><DataType>Bool</DataType><Normal>; </Normal><Keyword>var</Keyword><Normal> c: </Normal><DataType>Ref</DataType><Normal>; </Normal><Keyword>var</Keyword><Normal> d: </Normal><DataType>Rational</DataType><Normal>; </Normal><Keyword>var</Keyword><Normal> e: </Normal><DataType>Perm</DataType><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> x: </Normal><DataType>Seq</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>]; </Normal><Keyword>var</Keyword><Normal> y: </Normal><DataType>Set</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>]; </Normal><Keyword>var</Keyword><Normal> z: </Normal><DataType>Multiset</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>]</Normal><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> t1: </Normal><DataType>Set</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>] := </Normal><DataType>Set</DataType><Normal>(a, </Normal><DecVal>1</DecVal><Normal>, </Normal><DecVal>2</DecVal><Normal>)</Normal><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> t2: </Normal><DataType>Seq</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>] := </Normal><DataType>Seq</DataType><Normal>(a, a, a)</Normal><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> t3: </Normal><DataType>Multiset</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>] := </Normal><DataType>Multiset</DataType><Normal>(a, a, </Normal><DecVal>0</DecVal><Normal>, </Normal><DecVal>0</DecVal><Normal>, </Normal><DecVal>0</DecVal><Normal>)</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> myFunc(</Normal><DecVal>331</DecVal><Normal>) > -</Normal><DecVal>2</DecVal><br/>
<Normal></Normal><br/>
<Normal> myStmtMacro( myFunc(</Normal><DecVal>331</DecVal><Normal>) == -</Normal><DecVal>331</DecVal><Normal> )</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><ControlFlow>while</ControlFlow><Normal> ( </Normal><Constant>true</Constant><Normal> )</Normal><br/>
<Normal> </Normal><Keyword>invariant</Keyword><Normal> </Normal><Constant>true</Constant><br/>
<Normal> </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> aa: </Normal><DataType>Ref</DataType><br/>
<Normal> aa := </Normal><Constant>null</Constant><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> bb: </Normal><DataType>Int</DataType><br/>
<Normal> bb := </Normal><DecVal>33</DecVal><br/>
<Normal> </Normal><Operator>}</Operator><br/>
<Normal></Normal><br/>
<Normal> </Normal><ControlFlow>if</ControlFlow><Normal> ( </Normal><Constant>true</Constant><Normal> ) </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>true</Constant><br/>
<Normal> </Normal><Operator>}</Operator><Normal> </Normal><ControlFlow>elseif</ControlFlow><Normal> ( </Normal><Constant>false</Constant><Normal> ) </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>false</Constant><br/>
<Normal> </Normal><Operator>}</Operator><Normal> </Normal><ControlFlow>else</ControlFlow><Normal> </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>true</Constant><br/>
<Normal> </Normal><Operator>}</Operator><br/>
<Normal></Normal><br/>
<Normal> </Normal><Comment>//forperm r: Ref :: true</Comment><br/>
<Normal> </Normal><Comment>//exists</Comment><br/>
<Normal> </Normal><Comment>//forall</Comment><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> ! </Normal><Constant>false</Constant><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><DecVal>0</DecVal><Normal> +</Normal><DecVal>321</DecVal><Normal> - </Normal><DecVal>0</DecVal><Normal> -</Normal><DecVal>321</DecVal><Normal> == </Normal><DecVal>0</DecVal><br/>
<Operator>}</Operator><br/>
<Normal></Normal><br/>
<Keyword>field</Keyword><Normal> </Normal><Declaration>f</Declaration><Normal>:</Normal><DataType>Int</DataType><br/>
<Normal></Normal><br/>
<Keyword>method</Keyword><Normal> </Normal><Declaration>test02</Declaration><Normal>(x: </Normal><DataType>Ref</DataType><Normal>)</Normal><br/>
<Normal> </Normal><Keyword>requires</Keyword><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, </Normal><Keyword>write</Keyword><Normal>)</Normal><br/>
<Normal> </Normal><Keyword>ensures</Keyword><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, </Normal><Keyword>write</Keyword><Normal>)</Normal><br/>
<Operator>{</Operator><br/>
<Normal> </Normal><Keyword>define</Keyword><Normal> </Normal><Declaration>A</Declaration><Normal> </Normal><Constant>true</Constant><br/>
<Normal> </Normal><Keyword>define</Keyword><Normal> </Normal><Declaration>B</Declaration><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, </Normal><Keyword>write</Keyword><Normal>)</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>package</Keyword><Normal> A --* B</Normal><br/>
<Normal> </Normal><Keyword>wand</Keyword><Normal> w := A --* B</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Comment>//apply w</Comment><br/>
<Normal></Normal><br/>
<Normal> </Normal><ControlFlow>label</ControlFlow><Normal> my_lbl</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><ControlFlow>goto</ControlFlow><Normal> my_lbl</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>fresh</Keyword><Normal> x</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> p: </Normal><DataType>Perm</DataType><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>var</Keyword><Normal> r: </Normal><DataType>Ref</DataType><Normal>; r := new (*)</Normal><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>constraining</Keyword><Normal> ( p ) </Normal><Operator>{</Operator><br/>
<Normal> </Normal><Keyword>exhale</Keyword><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, p)</Normal><br/>
<Normal> </Normal><Operator>}</Operator><br/>
<Normal></Normal><br/>
<Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><DecVal>0</DecVal><Normal> == ( </Normal><Keyword>let</Keyword><Normal> a == (</Normal><DecVal>11</DecVal><Normal> + </Normal><DecVal>22</DecVal><Normal>) </Normal><Keyword>in</Keyword><Normal> a+a )</Normal><br/>
<Operator>}</Operator><br/>
|
