engine/tests/test1.tex

   1 \documentclass{article}
   2 \usepackage{fullpage}
   3
   4 \newcommand{\U}{\,\mbox{\sf{U}}\,}
   5 \newcommand{\A}{\mbox{\sf{A}}}
   6 \newcommand{\E}{\mbox{\sf{E}}}
   7 \newcommand{\AX}{\mbox{\sf{AX}}}
   8 \newcommand{\EX}{\mbox{\sf{EX}}}
   9 \newcommand{\AF}{\mbox{\sf{AF}}}
  10 \newcommand{\EF}{\mbox{\sf{EF}}}
  11 \newcommand{\AG}{\mbox{\sf{AG}}}
  12 \newcommand{\EG}{\mbox{\sf{EG}}}
  13
  14 \newcommand{\mita}[1]{\mbox{\it{{#1}}}}
  15 \newcommand{\mtt}[1]{\mbox{\tt{{#1}}}}
  16 \newcommand{\msf}[1]{\mbox{\sf{{#1}}}}
  17 \newcommand{\mrm}[1]{\mbox{\rm{{#1}}}}
  18 \newcommand{\mth}[1]{\({#1}\)}
  19
  20 \newcommand{\ttlb}{\mbox{\tt \char'173}}
  21 \newcommand{\ttrb}{\mbox{\tt \char'175}}
  22
  23 \begin{document}
  24
  25 \begin{quote}\begin{verbatim}
  26
  27 @@
  28 @@
  29
  30 f();
  31 ...
  32 ?g();
  33 ...
  34 h();
  35 \end{verbatim}\end{quote}
  36
  37 \[\begin{array}{l}
  38 \mita{\sf{let}} \, \mita{l9} = \mita{f();} \, \mita{\sf{in}} \, \mita{l9} \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \mita{g();} \, \mita{\sf{in}} \, \A[\neg (\mita{l0} \vee \mita{l9}) \U (\mita{\sf{let}} \, \mita{l7} = \msf{After}\\\mbox{} \vee \msf{ErrorExit} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l10} = (\mita{\sf{let}} \, \mita{l5} = \mita{h();} \, \mita{\sf{in}} \, \A[\neg (\mita{l5} \vee \mita{l0}) \U (\mita{l5} \vee \mita{l7})]
  39
  40 ) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l3} = \mita{l0}\\\mbox{} \wedge (\AX\mita{l10}) \, \mita{\sf{in}} \, \mita{l3} \vee ((\neg \mita{l3}) \wedge \mita{l10})
  41 )
  42 ) \vee \mita{l7}
  43 )]
  44
  45 ))
  46
  47 \end{array}\]
  48
  49 \begin{quote}\begin{verbatim}
  50
  51 @@
  52 @@
  53
  54 foo(...) {
  55
  56 (
  57   -f-(-3-, -E-)-;
  58     >>> f(3, 3, E);
  59
  60 |
  61   -f-(-E-, -4-)-;
  62     >>> f(E, 4, 4);
  63
  64 |
  65   -E-;
  66     >>> g(E);
  67
  68 )
  69
  70 (
  71   -f-(-3-, -X-)-;
  72     >>> f(3, 3, X);
  73
  74 |
  75   -f-(-Y-, -4-)-;
  76     >>> f(Y, 4, 4);
  77
  78 |
  79   -Z-;
  80     >>> g(Z);
  81
  82 )
  83
  84 (
  85   -f-(-3-)-;
  86     >>> f(3, 3);
  87
  88 |
  89   -f-(-4-)-;
  90     >>> f(4, 4);
  91
  92 )
  93 }
  94 \end{verbatim}\end{quote}
  95
  96 \[\begin{array}{l}
  97 (\exists \mita{foo} . \mita{foo(...) }) \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l17} = \msf{Paren}(p0) \, \mita{\sf{in}} \, \mita{{\ttlb}
  98   } \wedge \mita{l17} \wedge (\AX(\mita{\sf{let}} \, \mita{l32} = \AX(\mita{\sf{let}} \, \mita{l2} = \AX(\mita{\sf{let}} \, \mita{l12} = \AX(\mita{
  99 {\ttrb}}\\\mbox{} \wedge \mita{l17}) \, \mita{\sf{in}} \, ((\exists \mita{v0} . \mita{-f-(-3-)-;
 100   \mth{>}\mth{>}\mth{>} f(3, 3);}_{\mita{v0}}) \wedge \mita{l12}) \vee ((\exists \mita{v0} . \mita{-f-(-4-)-;
 101   \mth{>}\mth{>}\mth{>} f(4, 4);}_{\mita{v0}})\\\mbox{} \wedge \mita{l12})
 102 ) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l7} = \exists \mita{X} . \exists \mita{v0} . \mita{-f-(-3-, -X-)-;
 103   \mth{>}\mth{>}\mth{>} f(3, 3, X);}_{\mita{v0}} \, \mita{\sf{in}} \, (\mita{l7}\\\mbox{} \wedge \mita{l2}) \vee (\mita{\sf{let}} \, \mita{l21} = \neg \mita{l7} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l6} = \exists \mita{Y} . \exists \mita{v0} . \mita{-f-(-Y-, -4-)-;
 104   \mth{>}\mth{>}\mth{>} f(Y, 4, 4);}_{\mita{v0}}\\\mbox{} \, \mita{\sf{in}} \, (\mita{l21} \wedge \mita{l6} \wedge \mita{l2}) \vee ((\neg \mita{l6}) \wedge \mita{l21} \wedge (\exists \mita{Z} . \exists \mita{v0} . \mita{-Z-;
 105   \mth{>}\mth{>}\mth{>} g(Z);}_{\mita{v0}}) \wedge \mita{l2})
 106 )
 107 )
 108 )
 109 ) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l8} = \exists \mita{E}\\\mbox{} . \exists \mita{v0} . \mita{-f-(-3-, -E-)-;
 110   \mth{>}\mth{>}\mth{>} f(3, 3, E);}_{\mita{v0}} \, \mita{\sf{in}} \, (\mita{l8} \wedge \mita{l32}) \vee (\mita{\sf{let}} \, \mita{l19} = \neg \mita{l8}\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l4} = \exists \mita{E} . \exists \mita{v0} . \mita{-f-(-E-, -4-)-;
 111   \mth{>}\mth{>}\mth{>} f(E, 4, 4);}_{\mita{v0}} \, \mita{\sf{in}} \, (\mita{l19} \wedge \mita{l4}\\\mbox{} \wedge \mita{l32}) \vee ((\neg \mita{l4}) \wedge \mita{l19} \wedge (\exists \mita{E} . \exists \mita{v0} . \mita{-E-;
 112   \mth{>}\mth{>}\mth{>} g(E);}_{\mita{v0}}) \wedge \mita{l32})
 113 )
 114 )
 115 )
 116 ))
 117 )))
 118 \end{array}\]
 119
 120 \begin{quote}\begin{verbatim}
 121
 122 @@
 123 @@
 124
 125 p(
 126     <<< int hostptr,
 127   char buffer) {
 128   -int -hostptr-;
 129 }
 130 \end{verbatim}\end{quote}
 131
 132 \[\begin{array}{l}
 133 \exists \mita{hostptr} . ((\exists \mita{buffer} . \exists \mita{v0} . \mita{p(
 134     <<< int hostptr,
 135   char buffer) }_{\mita{v0}})\\\mbox{} \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l0} = \msf{Paren}(p0) \, \mita{\sf{in}} \, \mita{{\ttlb}
 136   } \wedge \mita{l0} \wedge (\AX((\exists \mita{v0} . \mita{-int -hostptr-;}_{\mita{v0}})\\\mbox{} \wedge (\AX(\mita{
 137 {\ttrb}} \wedge \mita{l0}))))
 138 ))))
 139 \end{array}\]
 140
 141 \begin{quote}\begin{verbatim}
 142
 143 @@
 144 @@
 145
 146 f(X);
 147 -...   WHEN != -h-(-X-)
 148 g(Y);
 149 \end{verbatim}\end{quote}
 150
 151 \[\begin{array}{l}
 152 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l1} = \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\exists \mita{v0} . \mita{-\_S0}_{\mita{v0}}) \wedge (\neg (\exists \mita{v0}\\\mbox{} . \mita{-h-(-X-)}_{\mita{v0}})) \wedge (\neg (\mita{l0} \vee \mita{l1}))) \U (\mita{l0} \vee \msf{After} \vee \msf{ErrorExit})]
 153
 154 ))
 155 )
 156 \end{array}\]
 157
 158 \begin{quote}\begin{verbatim}
 159
 160 @@
 161 @@
 162
 163 f(X);
 164 -...
 165 g(Y);
 166 \end{verbatim}\end{quote}
 167
 168 \[\begin{array}{l}
 169 \mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\exists \mita{v0} . \mita{-\_S0}_{\mita{v0}}) \wedge (\neg (\mita{l2}\\\mbox{} \vee \mita{l1}))) \U (\mita{l2} \vee \msf{After} \vee \msf{ErrorExit})]
 170
 171 ))
 172
 173 \end{array}\]
 174
 175 \begin{quote}\begin{verbatim}
 176
 177 @@
 178 @@
 179
 180 f(X);
 181 g(Y);
 182 h(X);
 183 f(Y);
 184 g(X);
 185 h(Y);
 186 \end{verbatim}\end{quote}
 187
 188 \[\begin{array}{l}
 189 \exists \mita{X} . (\mita{f(X);} \wedge (\AX(\exists \mita{Y} . (\mita{g(Y);} \wedge (\AX(\mita{h(X);} \wedge (\AX(\mita{f(Y);} \wedge (\AX(\mita{g(X);} \wedge (\AX(\mita{h(Y);}))))))))))))
 190 \end{array}\]
 191
 192 \begin{quote}\begin{verbatim}
 193
 194 @@
 195 @@
 196
 197 f(X);
 198 ...
 199 g(X);
 200 h(X);
 201 \end{verbatim}\end{quote}
 202
 203 \[\begin{array}{l}
 204 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \mita{f(X);} \, \mita{\sf{in}} \, \mita{l0} \wedge (\AX(\mita{\sf{let}} \, \mita{l1} = \mita{g(X);} \, \mita{\sf{in}} \, \A[\neg (\mita{l1} \vee \mita{l0}) \U ((\mita{l1} \wedge (\AX(\mita{h(X);})))\\\mbox{} \vee \msf{After} \vee \msf{ErrorExit})]
 205
 206 ))
 207 )
 208 \end{array}\]
 209
 210 \begin{quote}\begin{verbatim}
 211
 212 @@
 213 @@
 214
 215 if (X) {
 216   ...
 217 } else {
 218   ...
 219 }
 220 f(X);
 221 \end{verbatim}\end{quote}
 222
 223 \[\begin{array}{l}
 224 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \msf{FalseBranch} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l1} = \msf{After} \, \mita{\sf{in}} \, \mita{if (X) } \wedge (\AX(\mita{\sf{let}} \, \mita{l15} = \AX(\exists \mita{p0}\\\mbox{} . (\mita{\sf{let}} \, \mita{l7} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l14} = \mita{{\ttlb}
 225   } \wedge \mita{l7} \, \mita{\sf{in}} \, \mita{l14} \wedge (\AX(\mita{\sf{let}} \, \mita{l13} = \mita{
 226 {\ttrb}} \wedge \mita{l7}\\\mbox{} \, \mita{\sf{in}} \, \A[\neg (\mita{l13} \vee \mita{l14}) \U (\mita{l13} \vee \mita{l1} \vee \msf{ErrorExit})]
 227
 228 ))
 229 )
 230 )) \, \mita{\sf{in}} \, (\msf{TrueBranch} \wedge \mita{l15}) \vee (\mita{l0}\\\mbox{} \wedge \mita{l15}) \vee (\mita{l1} \wedge (\AX(\mita{f(X);})))
 231 )) \wedge (\EX\mita{l0}) \wedge (\EX\mita{l1})
 232 )
 233 )
 234 \end{array}\]
 235
 236 \begin{quote}\begin{verbatim}
 237
 238 @@
 239 @@
 240
 241 if (X) {
 242   ...
 243 }
 244 f(X);
 245 \end{verbatim}\end{quote}
 246
 247 \[\begin{array}{l}
 248 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \msf{After} \, \mita{\sf{in}} \, \mita{if (X) } \wedge (\AX((\msf{TrueBranch} \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l2} = \msf{Paren}(p0)\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l4} = \mita{{\ttlb}
 249   } \wedge \mita{l2} \, \mita{\sf{in}} \, \mita{l4} \wedge (\AX(\mita{\sf{let}} \, \mita{l3} = \mita{
 250 {\ttrb}} \wedge \mita{l2} \, \mita{\sf{in}} \, \A[\neg (\mita{l3} \vee \mita{l4}) \U (\mita{l3} \vee \mita{l0}\\\mbox{} \vee \msf{ErrorExit})]
 251
 252 ))
 253 )
 254 )))) \vee \msf{FallThrough} \vee (\mita{l0} \wedge (\AX(\mita{f(X);}))))) \wedge (\EX\mita{l0})
 255 )
 256 \end{array}\]
 257
 258 \begin{quote}\begin{verbatim}
 259
 260 @@
 261 @@
 262
 263 while (X) {
 264   ...
 265 }
 266 f(X);
 267 \end{verbatim}\end{quote}
 268
 269 \[\begin{array}{l}
 270 \exists \mita{X} . (\mita{while (X) } \wedge (\mita{\sf{let}} \, \mita{l0} = \msf{After} \, \mita{\sf{in}} \, (\AX((\msf{TrueBranch} \rightarrow (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l3} = \msf{Paren}(p0)\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l5} = \mita{{\ttlb}
 271   } \wedge \mita{l3} \, \mita{\sf{in}} \, \mita{l5} \wedge (\AX(\mita{\sf{let}} \, \mita{l4} = \mita{
 272 {\ttrb}} \wedge \mita{l3} \, \mita{\sf{in}} \, \A[\neg (\mita{l4} \vee \mita{l5}) \U (\mita{l4} \vee \mita{l0}\\\mbox{} \vee \msf{ErrorExit})]
 273
 274 ))
 275 )
 276 )))) \wedge (\mita{l0} \rightarrow (\AX(\mita{f(X);}))))) \wedge (\EX\mita{l0})
 277 ))
 278 \end{array}\]
 279
 280 \begin{quote}\begin{verbatim}
 281
 282 @@
 283 @@
 284
 285 while (X) {
 286   ...
 287 }
 288 \end{verbatim}\end{quote}
 289
 290 \[\begin{array}{l}
 291 (\exists \mita{X} . \mita{while (X) }) \wedge (\AX(\msf{TrueBranch} \rightarrow (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l1} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l4} = \mita{{\ttlb}
 292   }\\\mbox{} \wedge \mita{l1} \, \mita{\sf{in}} \, \mita{l4} \wedge (\AX(\mita{\sf{let}} \, \mita{l3} = \mita{
 293 {\ttrb}} \wedge \mita{l1} \, \mita{\sf{in}} \, \A[\neg (\mita{l3} \vee \mita{l4}) \U (\mita{l3} \vee \msf{After} \vee \msf{ErrorExit})]
 294 \\\mbox{}
 295 ))
 296 )
 297 )))))
 298 \end{array}\]
 299
 300 \begin{quote}\begin{verbatim}
 301
 302 @@
 303 @@
 304
 305 {
 306   ...   WHEN != g(Y)
 307   f(X);
 308   ...   WHEN != h(Y)
 309 }
 310 \end{verbatim}\end{quote}
 311
 312 \[\begin{array}{l}
 313 \exists \mita{p0} . (\mita{\sf{let}} \, \mita{l6} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l9} = \mita{{\ttlb}
 314   } \wedge \mita{l6} \, \mita{\sf{in}} \, \mita{l9} \wedge (\AX(\exists \mita{Y} . (\mita{\sf{let}} \, \mita{l3} = \exists \mita{X} . \mita{f(X);}\\\mbox{} \, \mita{\sf{in}} \, \A[((\neg \mita{g(Y)}) \wedge (\neg (\mita{l3} \vee \mita{l9}))) \U (\mita{\sf{let}} \, \mita{l5} = \msf{After} \vee \msf{ErrorExit} \, \mita{\sf{in}} \, (\mita{l3} \wedge (\AX(\mita{\sf{let}} \, \mita{l8} = \mita{
 315 {\ttrb}}\\\mbox{} \wedge \mita{l6} \, \mita{\sf{in}} \, \A[((\neg \mita{h(Y)}) \wedge (\neg (\mita{l8} \vee \mita{l3}))) \U (\mita{l8} \vee \mita{l5})]
 316
 317 ))) \vee \mita{l5}
 318 )]
 319
 320 )))
 321 )
 322 )
 323 \end{array}\]
 324
 325 \begin{quote}\begin{verbatim}
 326
 327 @@
 328 @@
 329
 330 f(X);
 331 ...
 332 -g-(-Y-)-;
 333   >>> h(X, Y);
 334
 335 \end{verbatim}\end{quote}
 336
 337 \[\begin{array}{l}
 338 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \mita{f(X);} \, \mita{\sf{in}} \, \mita{l0} \wedge (\AX\A[\neg ((\exists \mita{Y} . \mita{-g-(-Y-)-;
 339   \mth{>}\mth{>}\mth{>} h(X, Y);}) \vee \mita{l0})\\\mbox{} \U ((\exists \mita{Y} . \exists \mita{v0} . \mita{-g-(-Y-)-;
 340   \mth{>}\mth{>}\mth{>} h(X, Y);}_{\mita{v0}}) \vee \msf{After} \vee \msf{ErrorExit})]
 341 )
 342 )
 343 \end{array}\]
 344
 345 \begin{quote}\begin{verbatim}
 346
 347 @@
 348 @@
 349
 350 -f-(-X-)-;
 351   >>> f(Z);
 352
 353 -...
 354 g(Y);
 355 h(Z);
 356 \end{verbatim}\end{quote}
 357
 358 \[\begin{array}{l}
 359 \exists \mita{Z} . ((\exists \mita{X} . \exists \mita{v0} . \mita{-f-(-X-)-;
 360   \mth{>}\mth{>}\mth{>} f(Z);}_{\mita{v0}}) \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\exists \mita{v0}\\\mbox{} . \mita{-\_S0}_{\mita{v0}}) \wedge (\neg (\mita{l0} \vee (\exists \mita{X} . \mita{-f-(-X-)-;
 361   \mth{>}\mth{>}\mth{>} f(Z);})))) \U ((\mita{l0} \wedge (\AX(\mita{h(Z);})))\\\mbox{} \vee \msf{After} \vee \msf{ErrorExit})]
 362
 363 )))
 364 \end{array}\]
 365
 366 \begin{quote}\begin{verbatim}
 367
 368 @@
 369 @@
 370
 371 -f-(-X-)-;
 372   >>> f(Z);
 373
 374 ...
 375 g(Y);
 376 h(Z);
 377 \end{verbatim}\end{quote}
 378
 379 \[\begin{array}{l}
 380 \exists \mita{Z} . ((\exists \mita{X} . \exists \mita{v0} . \mita{-f-(-X-)-;
 381   \mth{>}\mth{>}\mth{>} f(Z);}_{\mita{v0}}) \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[\neg (\mita{l0}\\\mbox{} \vee (\exists \mita{X} . \mita{-f-(-X-)-;
 382   \mth{>}\mth{>}\mth{>} f(Z);})) \U ((\mita{l0} \wedge (\AX(\mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
 383 \\\mbox{}
 384 )))
 385 \end{array}\]
 386
 387 \begin{quote}\begin{verbatim}
 388
 389 @@
 390 @@
 391
 392 f(X);
 393 ...
 394 g(Y);
 395 h(Z);
 396 \end{verbatim}\end{quote}
 397
 398 \[\begin{array}{l}
 399 \mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[\neg (\mita{l2} \vee \mita{l1}) \U ((\mita{l2} \wedge (\AX(\exists \mita{Z}\\\mbox{} . \mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
 400
 401 ))
 402
 403 \end{array}\]
 404
 405 \begin{quote}\begin{verbatim}
 406
 407 @@
 408 @@
 409
 410 f(X);
 411 ...   WHEN != h(Z)
 412 g(Y);
 413 h(Z);
 414 \end{verbatim}\end{quote}
 415
 416 \[\begin{array}{l}
 417 \mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\exists \mita{Z} . (\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\neg \mita{h(Z)}) \wedge (\neg (\mita{l2} \vee \mita{l1})))\\\mbox{} \U ((\mita{l2} \wedge (\AX(\mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
 418
 419 )))
 420
 421 \end{array}\]
 422
 423 \begin{quote}\begin{verbatim}
 424
 425 @@
 426 @@
 427
 428 f(X);
 429 ...   WHEN != h(Q)
 430 g(Y);
 431 h(Z);
 432 \end{verbatim}\end{quote}
 433
 434 \[\begin{array}{l}
 435 \mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\neg (\exists \mita{Q} . \mita{h(Q)})) \wedge (\neg (\mita{l2}\\\mbox{} \vee \mita{l1}))) \U ((\mita{l2} \wedge (\AX(\exists \mita{Z} . \mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
 436
 437 ))
 438
 439 \end{array}\]
 440
 441 \begin{quote}\begin{verbatim}
 442
 443 @@
 444 @@
 445
 446 if (X) {
 447   ...
 448 } else {
 449   g(X);
 450 }
 451 h(Z);
 452 \end{verbatim}\end{quote}
 453
 454 \[\begin{array}{l}
 455 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \msf{FalseBranch} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l1} = \msf{After} \, \mita{\sf{in}} \, \mita{if (X) } \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \msf{Paren}(p0)\\\mbox{} \, \mita{\sf{in}} \, (\msf{TrueBranch} \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l6} = \mita{{\ttlb}
 456   } \wedge \mita{l2} \, \mita{\sf{in}} \, \mita{l6} \wedge (\AX(\mita{\sf{let}} \, \mita{l5} = \mita{
 457 {\ttrb}} \wedge \mita{l2} \, \mita{\sf{in}} \, \A[\neg (\mita{l5}\\\mbox{} \vee \mita{l6}) \U (\mita{l5} \vee \mita{l1} \vee \msf{ErrorExit})]
 458
 459 ))
 460 )))) \vee (\mita{l0} \wedge (\AX(\exists \mita{p0} . (\mita{{\ttlb}
 461   } \wedge \mita{l2} \wedge (\AX(\mita{g(X);} \wedge (\AX(\mita{
 462 {\ttrb}}\\\mbox{} \wedge \mita{l2})))))))) \vee (\mita{l1} \wedge (\AX(\exists \mita{Z} . \mita{h(Z);})))
 463 )) \wedge (\EX\mita{l0}) \wedge (\EX\mita{l1})
 464 )
 465 )
 466 \end{array}\]
 467
 468 \begin{quote}\begin{verbatim}
 469
 470 @@
 471 @@
 472
 473 <...
 474
 475 (
 476   h(X)
 477 |
 478   g(Y)
 479 )
 480 ...>
 481 \end{verbatim}\end{quote}
 482
 483 \[\begin{array}{l}
 484 \AG(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \exists \mita{X} . \mita{
 485 (
 486 h(X)
 487 |
 488 g(Y)
 489 )} \, \mita{\sf{in}} \, \mita{l2} \vee (\neg \mita{l2})
 490 )
 491 \end{array}\]
 492
 493 \begin{quote}\begin{verbatim}
 494
 495 @@
 496 @@
 497
 498 <...
 499
 500 (
 501   h(X)
 502 |
 503   g(Y)
 504 )
 505 ...>
 506 r(X);
 507 \end{verbatim}\end{quote}
 508
 509 \[\begin{array}{l}
 510 \exists \mita{X} . (\mita{\sf{let}} \, \mita{l1} = \mita{r(X);} \, \mita{\sf{in}} \, \A[((\neg \mita{l1}) \wedge (\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{
 511 (
 512 h(X)
 513 |
 514 g(Y)
 515 )} \, \mita{\sf{in}} \, \mita{l0} \vee (\neg \mita{l0})\\\mbox{}
 516 )) \U (\mita{l1} \vee \msf{After} \vee \msf{ErrorExit})]
 517
 518 )
 519 \end{array}\]
 520
 521 \begin{quote}\begin{verbatim}
 522
 523 @@
 524 @@
 525
 526
 527 (
 528 h(X)
 529 |
 530 g(Y)
 531 )
 532 \end{verbatim}\end{quote}
 533
 534 \[\begin{array}{l}
 535 \exists \mita{Y} . \exists \mita{X} . \mita{
 536 (
 537 h(X)
 538 |
 539 g(Y)
 540 )}
 541 \end{array}\]
 542
 543 \begin{quote}\begin{verbatim}
 544
 545 @@
 546 @@
 547
 548 m(Y);
 549 ?h(X);
 550 g(Y);
 551 \end{verbatim}\end{quote}
 552
 553 \[\begin{array}{l}
 554 \exists \mita{Y} . (\mita{m(Y);} \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \mita{g(Y);} \, \mita{\sf{in}} \, ((\exists \mita{X} . \mita{h(X);}) \wedge (\AX\mita{l0})) \vee \mita{l0}
 555 )))
 556 \end{array}\]
 557
 558 \begin{quote}\begin{verbatim}
 559
 560 @@
 561 @@
 562
 563 sht/*struct Scsi_Host_Template */.proc_info = proc_info_func;
 564 \end{verbatim}\end{quote}
 565
 566 \[\begin{array}{l}
 567 \exists \mita{proc\_info\_func} . \exists \mita{sht} . \mita{sht/*struct Scsi\_Host\_Template */.proc\_info = proc\_info\_func;}
 568 \end{array}\]
 569
 570 \begin{quote}\begin{verbatim}
 571
 572 @@
 573 @@
 574
 575 proc_info_func(char *buffer, char **start, off_t offset, int length,
 576                int hostno, int inout) {
 577   ...
 578   struct Scsi_Host *hostptr;
 579   ...
 580   hostptr = scsi_host_hn_get(hostno);
 581   ...
 582   ?if (hostptr == NULL) ?{
 583     ?...
 584   ?}
 585   ...
 586   ?scsi_host_put(hostptr);
 587   ...
 588 }
 589 \end{verbatim}\end{quote}
 590
 591 \[\begin{array}{l}
 592 \exists \mita{hostno} . ((\exists \mita{buffer} . \exists \mita{start} . \exists \mita{offset} . \exists \mita{length} . \exists \mita{inout} . \mita{proc\_info\_func(char *buffer, char **start, off\_t offset, int length,
 593                int hostno, int inout) })\\\mbox{} \wedge (\AX(\exists \mita{p1} . (\mita{\sf{let}} \, \mita{l33} = \msf{Paren}(p1) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l5} = \mita{{\ttlb}
 594   } \wedge \mita{l33} \, \mita{\sf{in}} \, \mita{l5} \wedge (\AX(\mita{\sf{let}} \, \mita{l53} = \mita{struct Scsi\_Host *hostptr;}\\\mbox{} \, \mita{\sf{in}} \, \A[\neg ((\exists \mita{hostptr} . \mita{l53}) \vee \mita{l5}) \U (\mita{\sf{let}} \, \mita{l1} = \msf{After} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l6} = \mita{l1} \vee \msf{ErrorExit}\\\mbox{} \, \mita{\sf{in}} \, (\exists \mita{hostptr} . (\mita{l53} \wedge (\AX(\mita{\sf{let}} \, \mita{l30} = \mita{hostptr = scsi\_host\_hn\_get(hostno);}\\\mbox{} \, \mita{\sf{in}} \, \A[\neg (\mita{l30} \vee \mita{l53}) \U ((\mita{l30} \wedge (\AX(\mita{\sf{let}} \, \mita{l32} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l50} = \mita{
 595 {\ttrb}} \wedge \mita{l32}\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l14} = \mita{l50} \vee \mita{l6} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l2} = \msf{FallThrough} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l29} = \mita{l2} \vee \mita{l1} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l51} = \mita{{\ttlb}
 596   }\\\mbox{} \wedge \mita{l32} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l0} = \msf{TrueBranch} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l52} = \mita{if (hostptr == NULL) } \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l20} = \mita{l52}\\\mbox{} \wedge (\AX((\mita{l0} \wedge (\AX(\exists \mita{p0} . (\mita{l51} \wedge (\AX\AF\mita{l14}))))) \vee \mita{l29})) \, \mita{\sf{in}} \, \A[\neg (\mita{l20} \vee \mita{l30}) \U ((\mita{\sf{let}} \, \mita{l8} = \mita{scsi\_host\_put(hostptr);}\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l11} = \A[\neg \mita{l8} \U \mita{l6}]
 597  \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l25} = \mita{l8} \wedge (\AX\mita{l11}) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l39} = \neg \mita{l25} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l13} = (\mita{\sf{let}} \, \mita{l48} = (\mita{\sf{let}} \, \mita{l4} = \mita{
 598 {\ttrb}}\\\mbox{} \wedge \mita{l33} \, \mita{\sf{in}} \, \A[\neg (\mita{l4} \vee \mita{l8}) \U (\mita{l4} \vee \mita{l6})]
 599
 600 ) \, \mita{\sf{in}} \, (\mita{l8} \wedge (\AX\mita{l48})) \vee (\mita{l39} \wedge \mita{l48})
 601 ) \vee \mita{l6} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l36} = \neg (\mita{l8}\\\mbox{} \vee \mita{l20}) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l34} = \mita{l0} \wedge (\AX(\exists \mita{p0} . (\mita{l51} \wedge (\AX\A[\neg (\mita{l50} \vee \mita{l51}) \U \mita{l14}]
 602 )))) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l16} = \EX\mita{l1}\\\mbox{} \, \mita{\sf{in}} \, (\mita{l52} \wedge (\AX(\mita{l34} \vee \mita{l2} \vee (\mita{l1} \wedge (\AX\A[\mita{l36} \U \mita{l13}]
 603 )))) \wedge \mita{l16}) \vee ((\neg (\mita{l52} \wedge (\AX(\mita{l34}\\\mbox{} \vee \mita{l2} \vee (\mita{l1} \wedge (\AX\A[\mita{l36} \U (\mita{l25} \vee (\mita{l39} \wedge \mita{l11}) \vee \mita{l6})]
 604 )))) \wedge \mita{l16})) \wedge (\A[\neg (\mita{l8} \vee (\mita{l52} \wedge (\AX(\mita{l34}\\\mbox{} \vee \mita{l29})))) \U \mita{l13}]
 605 ))
 606 )
 607 )
 608 )
 609 )
 610 )
 611 )
 612 )
 613 ) \vee \mita{l6})]
 614
 615 )
 616 )
 617 )
 618 )
 619 )
 620 )
 621 )
 622 )
 623 ))) \vee \mita{l6})]
 624
 625 )))) \vee \mita{l6}
 626 )
 627 )]
 628
 629 ))
 630 )
 631 ))))
 632 \end{array}\]
 633
 634 \begin{quote}\begin{verbatim}
 635
 636 @@
 637 @@
 638
 639 proc_info_func(...) {
 640   <...
 641
 642 (
 643     E->host_no == hostno
 644 |
 645     hostno
 646 )
 647   ...>
 648 }
 649 \end{verbatim}\end{quote}
 650
 651 \[\begin{array}{l}
 652 \mita{proc\_info\_func(...) } \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l3} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l6} = \mita{{\ttlb}
 653   } \wedge \mita{l3}\\\mbox{} \, \mita{\sf{in}} \, \mita{l6} \wedge (\AX(\mita{\sf{let}} \, \mita{l5} = \mita{
 654 {\ttrb}} \wedge \mita{l3} \, \mita{\sf{in}} \, \A[((\neg (\mita{l5} \vee \mita{l6})) \wedge (\mita{\sf{let}} \, \mita{l2} = \exists \mita{E} . \mita{
 655 (
 656 E-\mth{>}host\_no == hostno
 657 |
 658 hostno
 659 )}\\\mbox{} \, \mita{\sf{in}} \, \mita{l2} \vee (\neg \mita{l2})
 660 )) \U (\mita{l5} \vee \msf{After} \vee \msf{ErrorExit})]
 661
 662 ))
 663 )
 664 )))
 665 \end{array}\]
 666
 667 \end{document}