| 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} |