Warning, /frameworks/syntax-highlighting/autotests/reference/test.vpr.ref is written in an unsupported language. File is not indexed.
0001 <Keyword>import </Keyword><String>"foo.tdf"</String><br/>
0002 <Keyword>import </Keyword><String>"foo.txt"</String><br/>
0003 <Keyword>import </Keyword><String>"foo.txt"</String><br/>
0004 <Normal></Normal><br/>
0005 <Keyword>domain</Keyword><Normal> </Normal><Declaration>Foo[T]</Declaration><Normal> </Normal><Operator>{</Operator><br/>
0006 <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/>
0007 <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/>
0008 <Operator>}</Operator><br/>
0009 <Normal></Normal><br/>
0010 <Comment>// this is a comment</Comment><br/>
0011 <Normal></Normal><br/>
0012 <Comment>/* This is also</Comment><br/>
0013 <Comment> * another multi-line comment</Comment><br/>
0014 <Comment> * With a string "string" and</Comment><br/>
0015 <Comment> * an import "foo.bar" inside */</Comment><br/>
0016 <Normal></Normal><br/>
0017 <Comment>// Any copyright is dedicated to the Public Domain.</Comment><br/>
0018 <Comment>// http://creativecommons.org/publicdomain/zero/1.0/</Comment><br/>
0019 <Normal></Normal><br/>
0020 <Keyword>import </Keyword><String>"empty.sil"</String><br/>
0021 <Normal></Normal><br/>
0022 <Keyword>method</Keyword><Normal> </Normal><Declaration>test1</Declaration><Normal>(xs: </Normal><DataType>Seq</DataType><Normal>[</Normal><DataType>Ref</DataType><Normal>]) </Normal><Operator>{</Operator><br/>
0023 <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/>
0024 <Operator>}</Operator><br/>
0025 <Normal></Normal><br/>
0026 <Keyword>function</Keyword><Normal> </Normal><Declaration>$</Declaration><Normal>(n: </Normal><DataType>Ref</DataType><Normal>, m: </Normal><DataType>Ref</DataType><Normal>): Node</Normal><br/>
0027 <Normal></Normal><br/>
0028 <Keyword>domain</Keyword><Normal> </Normal><Declaration>Foo[T]</Declaration><Normal> </Normal><Operator>{</Operator><br/>
0029 <Normal> </Normal><Keyword>function</Keyword><Normal> </Normal><Declaration>enc</Declaration><Normal>(arg: T): Foo[T]</Normal><br/>
0030 <Normal> </Normal><Keyword>function</Keyword><Normal> </Normal><Declaration>dec</Declaration><Normal>(arg: Foo[T]): T</Normal><br/>
0031 <Normal></Normal><br/>
0032 <Normal> </Normal><Keyword>axiom</Keyword><Normal> </Normal><Declaration>ax_Dec</Declaration><Normal> </Normal><Operator>{</Operator><br/>
0033 <Normal> </Normal><Keyword>forall</Keyword><Normal> arg: T ::</Normal><br/>
0034 <Normal> dec( enc(arg) ) == arg</Normal><br/>
0035 <Normal> </Normal><Operator>}</Operator><br/>
0036 <Normal></Normal><br/>
0037 <Normal> </Normal><Keyword>axiom</Keyword><Normal> </Normal><Declaration>ax_Enc</Declaration><Normal> </Normal><Operator>{</Operator><br/>
0038 <Normal> </Normal><Keyword>forall</Keyword><Normal> arg: Foo[T] ::</Normal><br/>
0039 <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/>
0040 <Normal> </Normal><TriggerZone>{</TriggerZone><Normal> </Normal><Italic>dec(arg)</Italic><Normal> </Normal><TriggerZone>}</TriggerZone><br/>
0041 <Normal> enc( dec(arg) ) == arg</Normal><br/>
0042 <Normal> </Normal><Operator>}</Operator><br/>
0043 <Operator>}</Operator><br/>
0044 <Normal></Normal><br/>
0045 <Keyword>function</Keyword><Normal> </Normal><Declaration>myFunc</Declaration><Normal>(arg: </Normal><DataType>Int</DataType><Normal>): </Normal><DataType>Int</DataType><br/>
0046 <Normal> </Normal><Keyword>requires</Keyword><Normal> </Normal><Constant>true</Constant><Normal> || </Normal><Constant>false</Constant><br/>
0047 <Normal> </Normal><Keyword>ensures</Keyword><Normal> arg <= </Normal><DecVal>0</DecVal><Normal> ==> </Normal><Keyword>result</Keyword><Normal> == -</Normal><DecVal>1</DecVal><br/>
0048 <Normal> </Normal><Keyword>ensures</Keyword><Normal> arg > </Normal><DecVal>0</DecVal><Normal> ==> </Normal><Keyword>result</Keyword><Normal> == arg</Normal><br/>
0049 <Operator>{</Operator><br/>
0050 <Normal> arg > </Normal><DecVal>0</DecVal><Normal> ? arg : myFunc(arg - </Normal><DecVal>1</DecVal><Normal>)</Normal><br/>
0051 <Operator>}</Operator><br/>
0052 <Normal></Normal><br/>
0053 <Keyword>field</Keyword><Normal> </Normal><Declaration>value</Declaration><Normal>: </Normal><DataType>Int</DataType><br/>
0054 <Keyword>field</Keyword><Normal> </Normal><Declaration>next</Declaration><Normal>: </Normal><DataType>Ref</DataType><br/>
0055 <Normal></Normal><br/>
0056 <Keyword>predicate</Keyword><Normal> </Normal><Declaration>list</Declaration><Normal>(xs: </Normal><DataType>Ref</DataType><Normal>) </Normal><Operator>{</Operator><br/>
0057 <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/>
0058 <Normal> && ( list(xs</Normal><Field>.next</Field><Normal>) )</Normal><br/>
0059 <Operator>}</Operator><br/>
0060 <Normal></Normal><br/>
0061 <Keyword>define</Keyword><Normal> </Normal><Declaration>myPureMacro</Declaration><Normal>(abc) abc</Normal><br/>
0062 <Normal></Normal><br/>
0063 <Keyword>define</Keyword><Normal> </Normal><Declaration>myStmtMacro</Declaration><Normal>(abc) </Normal><Operator>{</Operator><br/>
0064 <Normal> </Normal><Keyword>inhale</Keyword><Normal> abc</Normal><br/>
0065 <Normal> </Normal><Keyword>exhale</Keyword><Normal> abc</Normal><br/>
0066 <Operator>}</Operator><br/>
0067 <Normal></Normal><br/>
0068 <Keyword>method</Keyword><Normal> </Normal><Declaration>smokeTest</Declaration><Normal>() </Normal><Operator>{</Operator><br/>
0069 <Normal></Normal><br/>
0070 <Normal> </Normal><Keyword>inhale</Keyword><Normal> </Normal><Constant>false</Constant><Normal>; </Normal><Keyword>exhale</Keyword><Normal> </Normal><Constant>false</Constant><br/>
0071 <Normal> </Normal><Keyword>assume</Keyword><Normal> </Normal><Constant>false</Constant><Normal>; </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>false</Constant><br/>
0072 <Normal></Normal><br/>
0073 <Normal> </Normal><Comment>//magic wands</Comment><br/>
0074 <Normal> </Normal><Keyword>var</Keyword><Normal> s: </Normal><DataType>Set</DataType><Normal>[</Normal><DataType>Int</DataType><Normal>]</Normal><br/>
0075 <Normal> </Normal><Keyword>assert</Keyword><Normal> s </Normal><Operator>setminus</Operator><Normal> s != s</Normal><br/>
0076 <Normal></Normal><br/>
0077 <Operator>}</Operator><br/>
0078 <Normal></Normal><br/>
0079 <Comment>//:: special comment</Comment><br/>
0080 <Comment>/*</Comment><br/>
0081 <Comment> gfdgfd</Comment><br/>
0082 <Comment>*/</Comment><br/>
0083 <Normal></Normal><br/>
0084 <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/>
0085 <Normal> </Normal><Keyword>requires</Keyword><Normal> </Normal><Constant>true</Constant><br/>
0086 <Normal> </Normal><Keyword>ensures</Keyword><Normal> </Normal><Constant>false</Constant><br/>
0087 <Operator>{</Operator><br/>
0088 <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/>
0089 <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/>
0090 <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/>
0091 <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/>
0092 <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/>
0093 <Normal></Normal><br/>
0094 <Normal> </Normal><Keyword>assert</Keyword><Normal> myFunc(</Normal><DecVal>331</DecVal><Normal>) > -</Normal><DecVal>2</DecVal><br/>
0095 <Normal></Normal><br/>
0096 <Normal> myStmtMacro( myFunc(</Normal><DecVal>331</DecVal><Normal>) == -</Normal><DecVal>331</DecVal><Normal> )</Normal><br/>
0097 <Normal></Normal><br/>
0098 <Normal> </Normal><ControlFlow>while</ControlFlow><Normal> ( </Normal><Constant>true</Constant><Normal> )</Normal><br/>
0099 <Normal> </Normal><Keyword>invariant</Keyword><Normal> </Normal><Constant>true</Constant><br/>
0100 <Normal> </Normal><Operator>{</Operator><br/>
0101 <Normal> </Normal><Keyword>var</Keyword><Normal> aa: </Normal><DataType>Ref</DataType><br/>
0102 <Normal> aa := </Normal><Constant>null</Constant><br/>
0103 <Normal> </Normal><Keyword>var</Keyword><Normal> bb: </Normal><DataType>Int</DataType><br/>
0104 <Normal> bb := </Normal><DecVal>33</DecVal><br/>
0105 <Normal> </Normal><Operator>}</Operator><br/>
0106 <Normal></Normal><br/>
0107 <Normal> </Normal><ControlFlow>if</ControlFlow><Normal> ( </Normal><Constant>true</Constant><Normal> ) </Normal><Operator>{</Operator><br/>
0108 <Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>true</Constant><br/>
0109 <Normal> </Normal><Operator>}</Operator><Normal> </Normal><ControlFlow>elseif</ControlFlow><Normal> ( </Normal><Constant>false</Constant><Normal> ) </Normal><Operator>{</Operator><br/>
0110 <Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>false</Constant><br/>
0111 <Normal> </Normal><Operator>}</Operator><Normal> </Normal><ControlFlow>else</ControlFlow><Normal> </Normal><Operator>{</Operator><br/>
0112 <Normal> </Normal><Keyword>assert</Keyword><Normal> </Normal><Constant>true</Constant><br/>
0113 <Normal> </Normal><Operator>}</Operator><br/>
0114 <Normal></Normal><br/>
0115 <Normal> </Normal><Comment>//forperm r: Ref :: true</Comment><br/>
0116 <Normal> </Normal><Comment>//exists</Comment><br/>
0117 <Normal> </Normal><Comment>//forall</Comment><br/>
0118 <Normal> </Normal><Keyword>assert</Keyword><Normal> ! </Normal><Constant>false</Constant><br/>
0119 <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/>
0120 <Operator>}</Operator><br/>
0121 <Normal></Normal><br/>
0122 <Keyword>field</Keyword><Normal> </Normal><Declaration>f</Declaration><Normal>:</Normal><DataType>Int</DataType><br/>
0123 <Normal></Normal><br/>
0124 <Keyword>method</Keyword><Normal> </Normal><Declaration>test02</Declaration><Normal>(x: </Normal><DataType>Ref</DataType><Normal>)</Normal><br/>
0125 <Normal> </Normal><Keyword>requires</Keyword><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, </Normal><Keyword>write</Keyword><Normal>)</Normal><br/>
0126 <Normal> </Normal><Keyword>ensures</Keyword><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, </Normal><Keyword>write</Keyword><Normal>)</Normal><br/>
0127 <Operator>{</Operator><br/>
0128 <Normal> </Normal><Keyword>define</Keyword><Normal> </Normal><Declaration>A</Declaration><Normal> </Normal><Constant>true</Constant><br/>
0129 <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/>
0130 <Normal></Normal><br/>
0131 <Normal> </Normal><Keyword>package</Keyword><Normal> A --* B</Normal><br/>
0132 <Normal> </Normal><Keyword>wand</Keyword><Normal> w := A --* B</Normal><br/>
0133 <Normal></Normal><br/>
0134 <Normal> </Normal><Comment>//apply w</Comment><br/>
0135 <Normal></Normal><br/>
0136 <Normal> </Normal><ControlFlow>label</ControlFlow><Normal> my_lbl</Normal><br/>
0137 <Normal></Normal><br/>
0138 <Normal> </Normal><ControlFlow>goto</ControlFlow><Normal> my_lbl</Normal><br/>
0139 <Normal></Normal><br/>
0140 <Normal> </Normal><Keyword>fresh</Keyword><Normal> x</Normal><br/>
0141 <Normal></Normal><br/>
0142 <Normal> </Normal><Keyword>var</Keyword><Normal> p: </Normal><DataType>Perm</DataType><br/>
0143 <Normal></Normal><br/>
0144 <Normal> </Normal><Keyword>var</Keyword><Normal> r: </Normal><DataType>Ref</DataType><Normal>; r := new (*)</Normal><br/>
0145 <Normal></Normal><br/>
0146 <Normal> </Normal><Keyword>constraining</Keyword><Normal> ( p ) </Normal><Operator>{</Operator><br/>
0147 <Normal> </Normal><Keyword>exhale</Keyword><Normal> </Normal><Keyword>acc</Keyword><Normal>(x</Normal><Field>.f</Field><Normal>, p)</Normal><br/>
0148 <Normal> </Normal><Operator>}</Operator><br/>
0149 <Normal></Normal><br/>
0150 <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/>
0151 <Operator>}</Operator><br/>