File indexing completed on 2024-05-12 04:02:10
0001 <!DOCTYPE html> 0002 <html><head> 0003 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/> 0004 <title>test.vpr</title> 0005 <meta name="generator" content="KF5::SyntaxHighlighting - Definition (Viper) - Theme (Breeze Light)"/> 0006 </head><body style="background-color:#ffffff;color:#1f1c1b"><pre> 0007 <span style="font-weight:bold">import </span><span style="color:#bf0303">"foo.tdf"</span> 0008 <span style="font-weight:bold">import </span><span style="color:#bf0303">"foo.txt"</span> 0009 <span style="font-weight:bold">import </span><span style="color:#bf0303">"foo.txt"</span> 0010 0011 <span style="font-weight:bold">domain</span> <span style="color:#644a9b">Foo[T]</span> <span style="color:#ca60ca">{</span> 0012 <span style="font-weight:bold">axiom</span> <span style="color:#644a9b">named</span> <span style="color:#ca60ca">{</span> <span style="font-weight:bold">forall</span> x: <span style="color:#0057ae">Int</span>:: <span style="color:#3daee9">{</span><span style="font-style:italic">lookup(x)</span><span style="color:#3daee9">}</span> len(lookup(x)) == foobar(x) <span style="color:#ca60ca">}</span> 0013 <span style="font-weight:bold">axiom</span> <span style="color:#ca60ca">{</span> <span style="font-weight:bold">forall</span> x: <span style="color:#0057ae">Int</span> :: <span style="color:#3daee9">{</span><span style="font-style:italic">lookup(x)</span><span style="color:#3daee9">}</span> <span style="color:#3daee9">{</span><span style="font-style:italic">len(lookup(x))</span><span style="color:#3daee9">}</span> len(lookup(x)) == foobar(x) <span style="color:#ca60ca">}</span> <span style="color:#898887">// anonymous</span> 0014 <span style="color:#ca60ca">}</span> 0015 0016 <span style="color:#898887">// this is a comment</span> 0017 0018 <span style="color:#898887">/* This is also</span> 0019 <span style="color:#898887"> * another multi-line comment</span> 0020 <span style="color:#898887"> * With a string "string" and</span> 0021 <span style="color:#898887"> * an import "foo.bar" inside */</span> 0022 0023 <span style="color:#898887">// Any copyright is dedicated to the Public Domain.</span> 0024 <span style="color:#898887">// http://creativecommons.org/publicdomain/zero/1.0/</span> 0025 0026 <span style="font-weight:bold">import </span><span style="color:#bf0303">"empty.sil"</span> 0027 0028 <span style="font-weight:bold">method</span> <span style="color:#644a9b">test1</span>(xs: <span style="color:#0057ae">Seq</span>[<span style="color:#0057ae">Ref</span>]) <span style="color:#ca60ca">{</span> 0029 <span style="font-weight:bold">inhale</span> <span style="font-weight:bold">forall</span> i: <span style="color:#0057ae">Int</span> :: 0 <= i && i < |xs| ==> xs[i]<span style="font-style:italic">.f</span> != <span style="color:#b08000">0</span> 0030 <span style="color:#ca60ca">}</span> 0031 0032 <span style="font-weight:bold">function</span> <span style="color:#644a9b">$</span>(n: <span style="color:#0057ae">Ref</span>, m: <span style="color:#0057ae">Ref</span>): Node 0033 0034 <span style="font-weight:bold">domain</span> <span style="color:#644a9b">Foo[T]</span> <span style="color:#ca60ca">{</span> 0035 <span style="font-weight:bold">function</span> <span style="color:#644a9b">enc</span>(arg: T): Foo[T] 0036 <span style="font-weight:bold">function</span> <span style="color:#644a9b">dec</span>(arg: Foo[T]): T 0037 0038 <span style="font-weight:bold">axiom</span> <span style="color:#644a9b">ax_Dec</span> <span style="color:#ca60ca">{</span> 0039 <span style="font-weight:bold">forall</span> arg: T :: 0040 dec( enc(arg) ) == arg 0041 <span style="color:#ca60ca">}</span> 0042 0043 <span style="font-weight:bold">axiom</span> <span style="color:#644a9b">ax_Enc</span> <span style="color:#ca60ca">{</span> 0044 <span style="font-weight:bold">forall</span> arg: Foo[T] :: 0045 <span style="color:#3daee9">{</span> <span style="font-style:italic">enc(</span> <span style="font-style:italic">dec(arg)</span> <span style="font-style:italic">),</span> <span style="font-style:italic">foo(bar,</span> <span style="font-style:italic">i)</span> <span style="color:#3daee9">}</span> 0046 <span style="color:#3daee9">{</span> <span style="font-style:italic">dec(arg)</span> <span style="color:#3daee9">}</span> 0047 enc( dec(arg) ) == arg 0048 <span style="color:#ca60ca">}</span> 0049 <span style="color:#ca60ca">}</span> 0050 0051 <span style="font-weight:bold">function</span> <span style="color:#644a9b">myFunc</span>(arg: <span style="color:#0057ae">Int</span>): <span style="color:#0057ae">Int</span> 0052 <span style="font-weight:bold">requires</span> <span style="color:#aa5500">true</span> || <span style="color:#aa5500">false</span> 0053 <span style="font-weight:bold">ensures</span> arg <= <span style="color:#b08000">0</span> ==> <span style="font-weight:bold">result</span> == -<span style="color:#b08000">1</span> 0054 <span style="font-weight:bold">ensures</span> arg > <span style="color:#b08000">0</span> ==> <span style="font-weight:bold">result</span> == arg 0055 <span style="color:#ca60ca">{</span> 0056 arg > <span style="color:#b08000">0</span> ? arg : myFunc(arg - <span style="color:#b08000">1</span>) 0057 <span style="color:#ca60ca">}</span> 0058 0059 <span style="font-weight:bold">field</span> <span style="color:#644a9b">value</span>: <span style="color:#0057ae">Int</span> 0060 <span style="font-weight:bold">field</span> <span style="color:#644a9b">next</span>: <span style="color:#0057ae">Ref</span> 0061 0062 <span style="font-weight:bold">predicate</span> <span style="color:#644a9b">list</span>(xs: <span style="color:#0057ae">Ref</span>) <span style="color:#ca60ca">{</span> 0063 <span style="font-weight:bold">acc</span>(xs<span style="font-style:italic">.value</span>) && <span style="font-weight:bold">acc</span>(xs<span style="font-style:italic">.next</span>) 0064 && ( list(xs<span style="font-style:italic">.next</span>) ) 0065 <span style="color:#ca60ca">}</span> 0066 0067 <span style="font-weight:bold">define</span> <span style="color:#644a9b">myPureMacro</span>(abc) abc 0068 0069 <span style="font-weight:bold">define</span> <span style="color:#644a9b">myStmtMacro</span>(abc) <span style="color:#ca60ca">{</span> 0070 <span style="font-weight:bold">inhale</span> abc 0071 <span style="font-weight:bold">exhale</span> abc 0072 <span style="color:#ca60ca">}</span> 0073 0074 <span style="font-weight:bold">method</span> <span style="color:#644a9b">smokeTest</span>() <span style="color:#ca60ca">{</span> 0075 0076 <span style="font-weight:bold">inhale</span> <span style="color:#aa5500">false</span>; <span style="font-weight:bold">exhale</span> <span style="color:#aa5500">false</span> 0077 <span style="font-weight:bold">assume</span> <span style="color:#aa5500">false</span>; <span style="font-weight:bold">assert</span> <span style="color:#aa5500">false</span> 0078 0079 <span style="color:#898887">//magic wands</span> 0080 <span style="font-weight:bold">var</span> s: <span style="color:#0057ae">Set</span>[<span style="color:#0057ae">Int</span>] 0081 <span style="font-weight:bold">assert</span> s <span style="color:#ca60ca">setminus</span> s != s 0082 0083 <span style="color:#ca60ca">}</span> 0084 0085 <span style="color:#898887">//:: special comment</span> 0086 <span style="color:#898887">/*</span> 0087 <span style="color:#898887"> gfdgfd</span> 0088 <span style="color:#898887">*/</span> 0089 0090 <span style="font-weight:bold">method</span> <span style="color:#644a9b">testHighlights</span>() <span style="font-weight:bold">returns</span> ( res: <span style="color:#0057ae">Set</span>[<span style="color:#0057ae">Seq</span>[<span style="color:#0057ae">Multiset</span>[Foo[<span style="color:#0057ae">Int</span>]]]] ) 0091 <span style="font-weight:bold">requires</span> <span style="color:#aa5500">true</span> 0092 <span style="font-weight:bold">ensures</span> <span style="color:#aa5500">false</span> 0093 <span style="color:#ca60ca">{</span> 0094 <span style="font-weight:bold">var</span> a: <span style="color:#0057ae">Int</span>; <span style="font-weight:bold">var</span> b: <span style="color:#0057ae">Bool</span>; <span style="font-weight:bold">var</span> c: <span style="color:#0057ae">Ref</span>; <span style="font-weight:bold">var</span> d: <span style="color:#0057ae">Rational</span>; <span style="font-weight:bold">var</span> e: <span style="color:#0057ae">Perm</span> 0095 <span style="font-weight:bold">var</span> x: <span style="color:#0057ae">Seq</span>[<span style="color:#0057ae">Int</span>]; <span style="font-weight:bold">var</span> y: <span style="color:#0057ae">Set</span>[<span style="color:#0057ae">Int</span>]; <span style="font-weight:bold">var</span> z: <span style="color:#0057ae">Multiset</span>[<span style="color:#0057ae">Int</span>] 0096 <span style="font-weight:bold">var</span> t1: <span style="color:#0057ae">Set</span>[<span style="color:#0057ae">Int</span>] := <span style="color:#0057ae">Set</span>(a, <span style="color:#b08000">1</span>, <span style="color:#b08000">2</span>) 0097 <span style="font-weight:bold">var</span> t2: <span style="color:#0057ae">Seq</span>[<span style="color:#0057ae">Int</span>] := <span style="color:#0057ae">Seq</span>(a, a, a) 0098 <span style="font-weight:bold">var</span> t3: <span style="color:#0057ae">Multiset</span>[<span style="color:#0057ae">Int</span>] := <span style="color:#0057ae">Multiset</span>(a, a, <span style="color:#b08000">0</span>, <span style="color:#b08000">0</span>, <span style="color:#b08000">0</span>) 0099 0100 <span style="font-weight:bold">assert</span> myFunc(<span style="color:#b08000">331</span>) > -<span style="color:#b08000">2</span> 0101 0102 myStmtMacro( myFunc(<span style="color:#b08000">331</span>) == -<span style="color:#b08000">331</span> ) 0103 0104 <span style="font-weight:bold">while</span> ( <span style="color:#aa5500">true</span> ) 0105 <span style="font-weight:bold">invariant</span> <span style="color:#aa5500">true</span> 0106 <span style="color:#ca60ca">{</span> 0107 <span style="font-weight:bold">var</span> aa: <span style="color:#0057ae">Ref</span> 0108 aa := <span style="color:#aa5500">null</span> 0109 <span style="font-weight:bold">var</span> bb: <span style="color:#0057ae">Int</span> 0110 bb := <span style="color:#b08000">33</span> 0111 <span style="color:#ca60ca">}</span> 0112 0113 <span style="font-weight:bold">if</span> ( <span style="color:#aa5500">true</span> ) <span style="color:#ca60ca">{</span> 0114 <span style="font-weight:bold">assert</span> <span style="color:#aa5500">true</span> 0115 <span style="color:#ca60ca">}</span> <span style="font-weight:bold">elseif</span> ( <span style="color:#aa5500">false</span> ) <span style="color:#ca60ca">{</span> 0116 <span style="font-weight:bold">assert</span> <span style="color:#aa5500">false</span> 0117 <span style="color:#ca60ca">}</span> <span style="font-weight:bold">else</span> <span style="color:#ca60ca">{</span> 0118 <span style="font-weight:bold">assert</span> <span style="color:#aa5500">true</span> 0119 <span style="color:#ca60ca">}</span> 0120 0121 <span style="color:#898887">//forperm r: Ref :: true</span> 0122 <span style="color:#898887">//exists</span> 0123 <span style="color:#898887">//forall</span> 0124 <span style="font-weight:bold">assert</span> ! <span style="color:#aa5500">false</span> 0125 <span style="font-weight:bold">assert</span> <span style="color:#b08000">0</span> +<span style="color:#b08000">321</span> - <span style="color:#b08000">0</span> -<span style="color:#b08000">321</span> == <span style="color:#b08000">0</span> 0126 <span style="color:#ca60ca">}</span> 0127 0128 <span style="font-weight:bold">field</span> <span style="color:#644a9b">f</span>:<span style="color:#0057ae">Int</span> 0129 0130 <span style="font-weight:bold">method</span> <span style="color:#644a9b">test02</span>(x: <span style="color:#0057ae">Ref</span>) 0131 <span style="font-weight:bold">requires</span> <span style="font-weight:bold">acc</span>(x<span style="font-style:italic">.f</span>, <span style="font-weight:bold">write</span>) 0132 <span style="font-weight:bold">ensures</span> <span style="font-weight:bold">acc</span>(x<span style="font-style:italic">.f</span>, <span style="font-weight:bold">write</span>) 0133 <span style="color:#ca60ca">{</span> 0134 <span style="font-weight:bold">define</span> <span style="color:#644a9b">A</span> <span style="color:#aa5500">true</span> 0135 <span style="font-weight:bold">define</span> <span style="color:#644a9b">B</span> <span style="font-weight:bold">acc</span>(x<span style="font-style:italic">.f</span>, <span style="font-weight:bold">write</span>) 0136 0137 <span style="font-weight:bold">package</span> A --* B 0138 <span style="font-weight:bold">wand</span> w := A --* B 0139 0140 <span style="color:#898887">//apply w</span> 0141 0142 <span style="font-weight:bold">label</span> my_lbl 0143 0144 <span style="font-weight:bold">goto</span> my_lbl 0145 0146 <span style="font-weight:bold">fresh</span> x 0147 0148 <span style="font-weight:bold">var</span> p: <span style="color:#0057ae">Perm</span> 0149 0150 <span style="font-weight:bold">var</span> r: <span style="color:#0057ae">Ref</span>; r := new (*) 0151 0152 <span style="font-weight:bold">constraining</span> ( p ) <span style="color:#ca60ca">{</span> 0153 <span style="font-weight:bold">exhale</span> <span style="font-weight:bold">acc</span>(x<span style="font-style:italic">.f</span>, p) 0154 <span style="color:#ca60ca">}</span> 0155 0156 <span style="font-weight:bold">assert</span> <span style="color:#b08000">0</span> == ( <span style="font-weight:bold">let</span> a == (<span style="color:#b08000">11</span> + <span style="color:#b08000">22</span>) <span style="font-weight:bold">in</span> a+a ) 0157 <span style="color:#ca60ca">}</span> 0158 </pre></body></html>