001 package escjava.backpred; 002 class DefaultUnivBackPred { 003 static String s = 004 "(PROMPT_OFF)\n" + 005 ";----------------------------------------------------------------------\n" + 006 "; \"Universal\", or class-independent part, of the background predicate\n" + 007 "\n" + 008 "; === ESCJ 8: Section 0.4\n" + 009 " \n" + 010 "(BG_PUSH (FORALL (m i x) (EQ (select (store m i x) i) x)))\n" + 011 "\n" + 012 "(BG_PUSH (FORALL (m i j x) \n" + 013 " (IMPLIES (NEQ i j)\n" + 014 " (EQ (select (store m i x) j)\n" + 015 " (select m j)))))\n" + 016 "\n" + 017 "(BG_PUSH (FORALL (m i j k x)\n" + 018 " (IMPLIES (OR (< k i) (< j k))\n" + 019 " (EQ (select (unset m i j) k) (select m k)))))\n" + 020 "\n" + 021 "; === ESCJ 8: Section 1.1\n" + 022 "\n" + 023 "(DEFPRED (<: t0 t1))\n" + 024 "\n" + 025 "; <: reflexive\n" + 026 "(BG_PUSH \n" + 027 " (FORALL (t)\n" + 028 " (PATS (<: t t))\n" + 029 " (<: t t)))\n" + 030 "\n" + 031 "; a special case, for which the above may not fire\n" + 032 "\n" + 033 "(BG_PUSH (<: |T_java.lang.Object| |T_java.lang.Object|))\n" + 034 "\n" + 035 "; <: transitive \n" + 036 "(BG_PUSH \n" + 037 " (FORALL (t0 t1 t2)\n" + 038 " (PATS (MPAT (<: t0 t1) (<: t1 t2)))\n" + 039 " (IMPLIES (AND (<: t0 t1) (<: t1 t2))\n" + 040 " (<: t0 t2))))\n" + 041 "\n" + 042 ";anti-symmetry\n" + 043 "(BG_PUSH\n" + 044 " (FORALL\n" + 045 " (t0 t1)\n" + 046 " (PATS (MPAT (<: t0 t1) (<: t1 t0)))\n" + 047 " (IMPLIES (AND (<: t0 t1) (<: t1 t0)) (EQ t0 t1))))\n" + 048 "\n" + 049 "; primitive types are final\n" + 050 "\n" + 051 "(BG_PUSH (FORALL (t) (PATS (<: t |T_boolean|))\n" + 052 " (IMPLIES (<: t |T_boolean|) (EQ t |T_boolean|))))\n" + 053 "(BG_PUSH (FORALL (t) (PATS (<: t |T_char|))\n" + 054 " (IMPLIES (<: t |T_char|) (EQ t |T_char|))))\n" + 055 "(BG_PUSH (FORALL (t) (PATS (<: t |T_byte|))\n" + 056 " (IMPLIES (<: t |T_byte|) (EQ t |T_byte|))))\n" + 057 "(BG_PUSH (FORALL (t) (PATS (<: t |T_short|))\n" + 058 " (IMPLIES (<: t |T_short|) (EQ t |T_short|))))\n" + 059 "(BG_PUSH (FORALL (t) (PATS (<: t |T_int|))\n" + 060 " (IMPLIES (<: t |T_int|) (EQ t |T_int|))))\n" + 061 "(BG_PUSH (FORALL (t) (PATS (<: t |T_long|))\n" + 062 " (IMPLIES (<: t |T_long|) (EQ t |T_long|))))\n" + 063 "(BG_PUSH (FORALL (t) (PATS (<: t |T_float|))\n" + 064 " (IMPLIES (<: t |T_float|) (EQ t |T_float|))))\n" + 065 "(BG_PUSH (FORALL (t) (PATS (<: t |T_double|))\n" + 066 " (IMPLIES (<: t |T_double|) (EQ t |T_double|))))\n" + 067 "(BG_PUSH (FORALL (t) (PATS (<: t |T_bigint|))\n" + 068 " (IMPLIES (<: t |T_bigint|) (EQ t |T_bigint|))))\n" + 069 "(BG_PUSH (FORALL (t) (PATS (<: t |T_real|))\n" + 070 " (IMPLIES (<: t |T_real|) (EQ t |T_real|))))\n" + 071 "\n" + 072 "; (New as of 12 Dec 2000)\n" + 073 "; primitive types have no proper supertypes\n" + 074 "\n" + 075 "(BG_PUSH (FORALL (t) (PATS (<: |T_boolean| t))\n" + 076 " (IMPLIES (<: |T_boolean| t) (EQ t |T_boolean|))))\n" + 077 "(BG_PUSH (FORALL (t) (PATS (<: |T_char| t))\n" + 078 " (IMPLIES (<: |T_char| t) (EQ t |T_char|))))\n" + 079 "(BG_PUSH (FORALL (t) (PATS (<: |T_byte| t))\n" + 080 " (IMPLIES (<: |T_byte| t) (EQ t |T_byte|))))\n" + 081 "(BG_PUSH (FORALL (t) (PATS (<: |T_short| t))\n" + 082 " (IMPLIES (<: |T_short| t) (EQ t |T_short|))))\n" + 083 "(BG_PUSH (FORALL (t) (PATS (<: |T_int| t))\n" + 084 " (IMPLIES (<: |T_int| t) (EQ t |T_int|))))\n" + 085 "(BG_PUSH (FORALL (t) (PATS (<: |T_long| t))\n" + 086 " (IMPLIES (<: |T_long| t) (EQ t |T_long|))))\n" + 087 "(BG_PUSH (FORALL (t) (PATS (<: |T_float| t))\n" + 088 " (IMPLIES (<: |T_float| t) (EQ t |T_float|))))\n" + 089 "(BG_PUSH (FORALL (t) (PATS (<: |T_double| t))\n" + 090 " (IMPLIES (<: |T_double| t) (EQ t |T_double|))))\n" + 091 "(BG_PUSH (FORALL (t) (PATS (<: |T_bigint| t))\n" + 092 " (IMPLIES (<: |T_bigint| t) (EQ t |T_bigint|))))\n" + 093 "(BG_PUSH (FORALL (t) (PATS (<: |T_real| t))\n" + 094 " (IMPLIES (<: |T_real| t) (EQ t |T_real|))))\n" + 095 " \n" + 096 "; === ESCJ 8: Section 1.2\n" + 097 "\n" + 098 "(BG_PUSH\n" + 099 " (FORALL (t0 t1 t2)\n" + 100 " (PATS (<: t0 (asChild t1 t2)))\n" + 101 " (IMPLIES\n" + 102 " (<: t0 (asChild t1 t2))\n" + 103 " (EQ (classDown t2 t0) (asChild t1 t2)))))\n" + 104 "\n" + 105 "; === ESCJ 8: Section 1.3\n" + 106 " \n" + 107 "; new\n" + 108 "\n" + 109 "(BG_PUSH \n" + 110 " (<: |T_java.lang.Cloneable| |T_java.lang.Object|))\n" + 111 "\n" + 112 "(BG_PUSH\n" + 113 " (FORALL (t)\n" + 114 " (PATS (|_array| t))\n" + 115 " (<: (|_array| t) |T_java.lang.Cloneable|)))\n" + 116 " \n" + 117 "(BG_PUSH\n" + 118 " (FORALL (t)\n" + 119 " (PATS (elemtype (|_array| t)))\n" + 120 " (EQ (elemtype (|_array| t)) t)))\n" + 121 "\n" + 122 "(BG_PUSH\n" + 123 " (FORALL (t0 t1) \n" + 124 " (PATS (<: t0 (|_array| t1)))\n" + 125 " (IFF (<: t0 (|_array| t1))\n" + 126 " (AND\n" + 127 " (EQ t0 (|_array| (elemtype t0)))\n" + 128 " (<: (elemtype t0) t1)))))\n" + 129 "\n" + 130 "; === ESCJ 8: Section 2.1\n" + 131 "\n" + 132 "(DEFPRED (is x t))\n" + 133 "\n" + 134 "(BG_PUSH\n" + 135 " (FORALL (x t)\n" + 136 " (PATS (cast x t))\n" + 137 " (is (cast x t) t)))\n" + 138 " \n" + 139 "(BG_PUSH\n" + 140 " (FORALL (x t)\n" + 141 " (PATS (cast x t))\n" + 142 " (IMPLIES (is x t) (EQ (cast x t) x))))\n" + 143 " \n" + 144 "; === ESCJ 8: Section 2.2\n" + 145 "\n" + 146 "(BG_PUSH (DISTINCT |bool$false| |@true|))\n" + 147 "\n" + 148 "; === ESCJ 8: Section 2.2.1\n" + 149 "\n" + 150 "(BG_PUSH (FORALL (x) \n" + 151 " (PATS (is x |T_char|)) \n" + 152 " (IFF (is x |T_char|) (AND (<= 0 x) (<= x 65535)))))\n" + 153 "(BG_PUSH (FORALL (x)\n" + 154 " (PATS (is x |T_byte|))\n" + 155 " (IFF (is x |T_byte|) (AND (<= -128 x) (<= x 127)))))\n" + 156 "(BG_PUSH (FORALL (x) \n" + 157 " (PATS (is x |T_short|))\n" + 158 " (IFF (is x |T_short|) (AND (<= -32768 x) (<= x 32767)))))\n" + 159 "(BG_PUSH (FORALL (x) \n" + 160 " (PATS (is x |T_int|))\n" + 161 " (IFF (is x |T_int|) (AND (<= intFirst x) (<= x intLast)))))\n" + 162 "(BG_PUSH (FORALL (x) \n" + 163 " (PATS (is x |T_long|))\n" + 164 " (IFF (is x |T_long|) (AND (<= longFirst x) (<= x longLast)))))\n" + 165 "\n" + 166 "(BG_PUSH (< longFirst intFirst))\n" + 167 "(BG_PUSH (< intFirst -1000000))\n" + 168 "(BG_PUSH (< 1000000 intLast))\n" + 169 "(BG_PUSH (< intLast longLast))\n" + 170 "\n" + 171 "; === Define typeof for primitive types - DRCok\n" + 172 "\n" + 173 "(BG_PUSH (EQ |T_bigint| |T_long|)) ; FIXME - change this eventually\n" + 174 "\n" + 175 "(BG_PUSH (FORALL (x) \n" + 176 " (PATS (typeof x))\n" + 177 " (IFF (is x |T_int|) (EQ (typeof x) |T_int|))\n" + 178 " ))\n" + 179 "(BG_PUSH (FORALL (x) \n" + 180 " (PATS (typeof x))\n" + 181 " ;(PATS (is x |T_short|))\n" + 182 " (IFF (is x |T_short|) (EQ (typeof x) |T_short|))\n" + 183 " ))\n" + 184 "(BG_PUSH (FORALL (x) \n" + 185 " (PATS (typeof x))\n" + 186 " ;(PATS (is x |T_long|))\n" + 187 " (IFF (is x |T_long|) (EQ (typeof x) |T_long|))\n" + 188 " ))\n" + 189 "(BG_PUSH (FORALL (x) \n" + 190 " (PATS (typeof x))\n" + 191 " ;(PATS (is x |T_byte|))\n" + 192 " (IFF (is x |T_byte|) (EQ (typeof x) |T_byte|))\n" + 193 " ))\n" + 194 "(BG_PUSH (FORALL (x) \n" + 195 " (PATS (typeof x))\n" + 196 " ;(PATS (is x |T_char|))\n" + 197 " (IFF (is x |T_char|) (EQ (typeof x) |T_char|))\n" + 198 " ))\n" + 199 "(BG_PUSH (FORALL (x) \n" + 200 " (PATS (typeof x))\n" + 201 " ;(PATS (is x |T_boolean|))\n" + 202 " (IFF (is x |T_boolean|) (EQ (typeof x) |T_boolean|))\n" + 203 " ))\n" + 204 "(BG_PUSH (FORALL (x) \n" + 205 " (PATS (typeof x))\n" + 206 " ;(PATS (is x |T_double|))\n" + 207 " (IFF (is x |T_double|) (EQ (typeof x) |T_double|))\n" + 208 " ))\n" + 209 "(BG_PUSH (FORALL (x) \n" + 210 " (PATS (typeof x))\n" + 211 " ;(PATS (is x |T_float|))\n" + 212 " (IFF (is x |T_float|) (EQ (typeof x) |T_float|))\n" + 213 " ))\n" + 214 "(BG_PUSH (FORALL (x) \n" + 215 " (PATS (typeof x))\n" + 216 " ;(PATS (is x |T_real|))\n" + 217 " (IFF (is x |T_real|) (EQ (typeof x) |T_real|))\n" + 218 " ))\n" + 219 "(BG_PUSH (FORALL (x) \n" + 220 " (PATS (typeof x))\n" + 221 " ;(PATS (is x |T_bigint|))\n" + 222 " (IFF (is x |T_bigint|) (EQ (typeof x) |T_bigint|))\n" + 223 " ))\n" + 224 " \n" + 225 "; === ESCJ 8: Section 2.3\n" + 226 " \n" + 227 "(BG_PUSH\n" + 228 " (FORALL (x t)\n" + 229 " (PATS (MPAT (<: t |T_java.lang.Object|) (is x t)))\n" + 230 " (IMPLIES (<: t |T_java.lang.Object|)\n" + 231 " (IFF (is x t)\n" + 232 " (OR (EQ x null) (<: (typeof x) t))))))\n" + 233 "\n" + 234 "; === ESCJ 8: Section 2.4\n" + 235 "\n" + 236 "(BG_PUSH\n" + 237 " (FORALL (f t x) (PATS (select (asField f t) x))\n" + 238 " (is (select (asField f t) x) t)))\n" + 239 "\n" + 240 "; === ESCJ 8: Section 2.5\n" + 241 "\n" + 242 "(BG_PUSH\n" + 243 " (FORALL (e a i) (PATS (select (select (asElems e) a) i))\n" + 244 " (is (select (select (asElems e) a) i)\n" + 245 " (elemtype (typeof a)))))\n" + 246 "\n" + 247 "; === ESCJ 8: Section 3.0\n" + 248 "\n" + 249 "(DEFPRED (isAllocated x a0) (< (vAllocTime x) a0))\n" + 250 "\n" + 251 "; === ESCJ 8: Section 3.1\n" + 252 "\n" + 253 "(BG_PUSH\n" + 254 " (FORALL (x f a0) (PATS (isAllocated (select f x) a0))\n" + 255 " (IMPLIES (AND (< (fClosedTime f) a0)\n" + 256 " (isAllocated x a0))\n" + 257 " (isAllocated (select f x) a0))))\n" + 258 "\n" + 259 "; === ESCJ 8: Section 3.2\n" + 260 "\n" + 261 "(BG_PUSH\n" + 262 " (FORALL (a e i a0) (PATS (isAllocated (select (select e a) i) a0))\n" + 263 " (IMPLIES (AND (< (eClosedTime e) a0)\n" + 264 " (isAllocated a a0))\n" + 265 " (isAllocated (select (select e a) i) a0))))\n" + 266 " \n" + 267 "; === ESCJ 8: Section 4 \n" + 268 "\n" + 269 "; max(lockset) is in lockset\n" + 270 "\n" + 271 "(BG_PUSH\n" + 272 " (FORALL (S)\n" + 273 " (PATS (select (asLockSet S) (max (asLockSet S))))\n" + 274 " (EQ\n" + 275 " (select (asLockSet S) (max (asLockSet S)))\n" + 276 " |@true|)))\n" + 277 "\n" + 278 "; null is in lockset (not in ESCJ 8)\n" + 279 "\n" + 280 "(BG_PUSH\n" + 281 " (FORALL (S)\n" + 282 " (PATS (asLockSet S))\n" + 283 " (EQ (select (asLockSet S) null) |@true|)))\n" + 284 "\n" + 285 "(DEFPRED (lockLE x y) (<= x y))\n" + 286 "\n" + 287 "(DEFPRED (lockLT x y) (< x y))\n" + 288 "\n" + 289 "; all locks in lockset are below max(lockset) (not in ESCJ 8)\n" + 290 "\n" + 291 "(BG_PUSH\n" + 292 " (FORALL (S mu)\n" + 293 " (IMPLIES\n" + 294 " (EQ (select (asLockSet S) mu) |@true|)\n" + 295 " (lockLE mu (max (asLockSet S))))))\n" + 296 "\n" + 297 "; null precedes all objects in locking order (not in ESCJ 8)\n" + 298 "\n" + 299 "(BG_PUSH\n" + 300 " (FORALL (x)\n" + 301 " (PATS (lockLE null x) (lockLT null x) (lockLE x null) (lockLT x null))\n" + 302 " (IMPLIES\n" + 303 " (<: (typeof x) |T_java.lang.Object|)\n" + 304 " (lockLE null x))))\n" + 305 "\n" + 306 "\n" + 307 "; === ESCJ 8: Section 5.0\n" + 308 "\n" + 309 "(BG_PUSH\n" + 310 " (FORALL (a) \n" + 311 " (PATS (arrayLength a))\n" + 312 " (AND (<= 0 (arrayLength a))\n" + 313 " (is (arrayLength a) |T_int|))))\n" + 314 "\n" + 315 "(DEFPRED (arrayFresh a a0 b0 e s T v))\n" + 316 "\n" + 317 "(BG_PUSH\n" + 318 " (FORALL (a a0 b0 e n s T v)\n" + 319 " (PATS (arrayFresh a a0 b0 e (arrayShapeMore n s) T v))\n" + 320 " (IFF\n" + 321 " (arrayFresh a a0 b0 e (arrayShapeMore n s) T v)\n" + 322 " (AND\n" + 323 " (<= a0 (vAllocTime a))\n" + 324 " (isAllocated a b0)\n" + 325 " (NEQ a null)\n" + 326 " (EQ (typeof a) T)\n" + 327 " (EQ (arrayLength a) n)\n" + 328 " (FORALL (i)\n" + 329 " (PATS (select (select e a) i))\n" + 330 " (AND\n" + 331 " (arrayFresh (select (select e a) i) a0 b0 e s (elemtype T) v)\n" + 332 " (EQ (arrayParent (select (select e a) i)) a)\n" + 333 " (EQ (arrayPosition (select (select e a) i)) i)))))))\n" + 334 "\n" + 335 "(BG_PUSH\n" + 336 " (FORALL (a a0 b0 e n T v)\n" + 337 " (PATS (arrayFresh a a0 b0 e (arrayShapeOne n) T v))\n" + 338 " (IFF\n" + 339 " (arrayFresh a a0 b0 e (arrayShapeOne n) T v)\n" + 340 " (AND\n" + 341 " (<= a0 (vAllocTime a))\n" + 342 " (isAllocated a b0)\n" + 343 " (NEQ a null)\n" + 344 " (EQ (typeof a) T)\n" + 345 " (EQ (arrayLength a) n)\n" + 346 " (FORALL (i)\n" + 347 " (PATS (select (select e a) i))\n" + 348 " (AND\n" + 349 " (EQ (select (select e a) i) v)))))))\n" + 350 "\n" + 351 "\n" + 352 "(BG_PUSH\n" + 353 " (FORALL (a0 b0 e s T v)\n" + 354 " (PATS (arrayMake a0 b0 s T v))\n" + 355 " (arrayFresh\n" + 356 " (arrayMake a0 b0 s T v)\n" + 357 " a0 b0 elems s T v )\n" + 358 "))\n" + 359 "\n" + 360 "(BG_PUSH\n" + 361 " (FORALL (a0 b0 a1 b1 s1 s2 T1 T2 v)\n" + 362 " (PATS (MPAT (arrayMake a0 b0 s1 T1 v) (arrayMake a1 b1 s2 T2 v) ))\n" + 363 " (IMPLIES\n" + 364 " (EQ (arrayMake a0 b0 s1 T1 v) (arrayMake a1 b1 s2 T2 v))\n" + 365 " (AND (EQ b0 b1) (EQ T1 T2) (EQ s1 s2))\n" + 366 ")))\n" + 367 "\n" + 368 "; === code to ensure that (isNewArray x) ==> x has no invariants\n" + 369 "\n" + 370 "\n" + 371 "; arrayType is distinct from all types with invariants (due to the\n" + 372 "; generated type-distinctness axiom)\n" + 373 "\n" + 374 "(BG_PUSH\n" + 375 " (EQ arrayType (asChild arrayType |T_java.lang.Object|)))\n" + 376 "\n" + 377 "(BG_PUSH\n" + 378 " (FORALL (t)\n" + 379 " (PATS (|_array| t))\n" + 380 " (<: (|_array| t) arrayType)))\n" + 381 "\n" + 382 "(BG_PUSH\n" + 383 " (FORALL (s)\n" + 384 " (PATS (isNewArray s))\n" + 385 " (IMPLIES (EQ |@true| (isNewArray s))\n" + 386 " (<: (typeof s) arrayType))))\n" + 387 "\n" + 388 "; === ESCJ 8: Section 5.1\n" + 389 "\n" + 390 "(BG_PUSH\n" + 391 " (FORALL (i j) (PATS (integralMod i j) (integralDiv i j))\n" + 392 " (EQ (+ (* (integralDiv i j) j) (integralMod i j))\n" + 393 " i)))\n" + 394 "\n" + 395 "(BG_PUSH\n" + 396 " (FORALL (i j) (PATS (integralMod i j))\n" + 397 " (IMPLIES (< 0 j)\n" + 398 " (AND (<= 0 (integralMod i j))\n" + 399 " (< (integralMod i j) j)))))\n" + 400 "\n" + 401 "(BG_PUSH\n" + 402 " (FORALL (i j) (PATS (integralMod i j))\n" + 403 " (IMPLIES (< j 0)\n" + 404 " (AND (< j (integralMod i j))\n" + 405 " (<= (integralMod i j) 0)))))\n" + 406 "\n" + 407 "(BG_PUSH\n" + 408 " (FORALL (i j) \n" + 409 " (PATS (integralMod (+ i j) j))\n" + 410 " (EQ (integralMod (+ i j) j) \n" + 411 " (integralMod i j))))\n" + 412 "\n" + 413 "(BG_PUSH\n" + 414 " (FORALL (i j)\n" + 415 " (PATS (integralMod (+ j i) j))\n" + 416 " (EQ (integralMod (+ j i) j) \n" + 417 " (integralMod i j))))\n" + 418 "\n" + 419 "(BG_PUSH \n" + 420 " (FORALL (i)\n" + 421 " (PATS (integralMod 0 i))\n" + 422 " (IMPLIES (NOT (EQ i 0))\n" + 423 " (EQ (integralMod 0 i) 0)\n" + 424 " )))\n" + 425 "; to prevent a matching loop\n" + 426 "(BG_PUSH\n" + 427 " (FORALL (x y)\n" + 428 " (PATS (* (integralDiv (* x y) y) y))\n" + 429 " (EQ (* (integralDiv (* x y) y) y) (* x y))))\n" + 430 "\n" + 431 "\n" + 432 "; === ESCJ 8: Section 5.2\n" + 433 "\n" + 434 "(DEFPRED (boolAnd a b)\n" + 435 " (AND\n" + 436 " (EQ a |@true|) \n" + 437 " (EQ b |@true|)))\n" + 438 "\n" + 439 "(DEFPRED (boolEq a b)\n" + 440 " (IFF\n" + 441 " (EQ a |@true|)\n" + 442 " (EQ b |@true|)))\n" + 443 "\n" + 444 "(DEFPRED (boolImplies a b)\n" + 445 " (IMPLIES\n" + 446 " (EQ a |@true|)\n" + 447 " (EQ b |@true|)))\n" + 448 " \n" + 449 "(DEFPRED (boolNE a b)\n" + 450 " (NOT (IFF\n" + 451 " (EQ a |@true|)\n" + 452 " (EQ b |@true|))))\n" + 453 "\n" + 454 "(DEFPRED (boolNot a)\n" + 455 " (NOT (EQ a |@true|)))\n" + 456 "\n" + 457 "(DEFPRED (boolOr a b)\n" + 458 " (OR\n" + 459 " (EQ a |@true|)\n" + 460 " (EQ b |@true|)))\n" + 461 "\n" + 462 "; Axioms related to Strings - DRCok\n" + 463 "\n" + 464 "(DEFPRED (|interned:| s))\n" + 465 "\n" + 466 "(BG_PUSH\n" + 467 " (FORALL (i k)\n" + 468 " (PATS (|intern:| i k))\n" + 469 " (AND (NEQ (|intern:| i k) null)\n" + 470 " (EQ (typeof (|intern:| i k)) |T_java.lang.String|)\n" + 471 " (isAllocated (|intern:| i k) alloc))))\n" + 472 "\n" + 473 "(BG_PUSH\n" + 474 " (FORALL (s)\n" + 475 " (PATS (|interned:| s))\n" + 476 " (is (|interned:| s) |T_boolean|)\n" + 477 " ))\n" + 478 "\n" + 479 "(BG_PUSH\n" + 480 " (FORALL (i ii k kk)\n" + 481 " (PATS (MPAT (|intern:| i k) (|intern:| ii kk)))\n" + 482 " (IFF (EQ (|intern:| i k) (|intern:| ii kk)) (EQ i ii)) ))\n" + 483 "\n" + 484 "(BG_PUSH\n" + 485 " (FORALL (i k)\n" + 486 " (PATS (|intern:| i k))\n" + 487 " (|interned:| (|intern:| i k))\n" + 488 " ))\n" + 489 " \n" + 490 "(BG_PUSH\n" + 491 " (FORALL (x y a)\n" + 492 " (PATS (stringCat x y a))\n" + 493 " (AND (NEQ (stringCat x y a) null)\n" + 494 " (NOT (isAllocated (stringCat x y a) a))\n" + 495 " (EQ (typeof (stringCat x y a)) |T_java.lang.String|))))\n" + 496 "\n" + 497 "(BG_PUSH\n" + 498 " (FORALL (x y a b)\n" + 499 " (PATS (MPAT (stringCat x y a) (stringCat x y b)))\n" + 500 " (IFF (EQ (stringCat x y a) (stringCat x y b)) (EQ a b))))\n" + 501 "\n" + 502 "(BG_PUSH\n" + 503 " (FORALL (a b i j)\n" + 504 " (PATS (MPAT (next a i) (next b j)))\n" + 505 " (IFF (EQ (next a i)(next b j))\n" + 506 " (AND (EQ a b)(EQ i j)))))\n" + 507 " \n" + 508 "(BG_PUSH\n" + 509 " (FORALL (a i) \n" + 510 " (PATS (next a i))\n" + 511 " (< a (next a i))))\n" + 512 " \n" + 513 "(BG_PUSH\n" + 514 " (FORALL (x y xx yy a b)\n" + 515 " (PATS (MPAT (stringCat x y a) (stringCat xx yy b)))\n" + 516 " (IMPLIES\n" + 517 " (EQ (stringCat x y a) (stringCat xx yy b))\n" + 518 " (EQ a b))))\n" + 519 " \n" + 520 "(DEFPRED (stringCatP r x y a0 a1))\n" + 521 "\n" + 522 "(BG_PUSH\n" + 523 " (FORALL (r x y a0 a1)\n" + 524 " (PATS (stringCatP r x y a0 a1))\n" + 525 " (IMPLIES (stringCatP r x y a0 a1)\n" + 526 " (AND (NEQ r null)\n" + 527 " (isAllocated r a1)\n" + 528 " (NOT (isAllocated r a0))\n" + 529 " (< a0 a1)\n" + 530 " (EQ (typeof r) |T_java.lang.String|)))))\n" + 531 "\n" + 532 "; Not in ESCJ8, but should be\n" + 533 "\n" + 534 "(BG_PUSH\n" + 535 " (FORALL (x y)\n" + 536 " (PATS (integralEQ x y))\n" + 537 " (IFF\n" + 538 " (EQ (integralEQ x y) |@true|)\n" + 539 " (EQ x y))))\n" + 540 "\n" + 541 "(BG_PUSH\n" + 542 " (FORALL (x y)\n" + 543 " (PATS (integralGE x y))\n" + 544 " (IFF\n" + 545 " (EQ (integralGE x y) |@true|)\n" + 546 " (>= x y))))\n" + 547 "\n" + 548 "(BG_PUSH\n" + 549 " (FORALL (x y)\n" + 550 " (PATS (integralGT x y))\n" + 551 " (IFF\n" + 552 " (EQ (integralGT x y) |@true|)\n" + 553 " (> x y))))\n" + 554 "\n" + 555 "(BG_PUSH\n" + 556 " (FORALL (x y)\n" + 557 " (PATS (integralLE x y))\n" + 558 " (IFF\n" + 559 " (EQ (integralLE x y) |@true|)\n" + 560 " (<= x y))))\n" + 561 "\n" + 562 "(BG_PUSH\n" + 563 " (FORALL (x y)\n" + 564 " (PATS (integralLT x y))\n" + 565 " (IFF\n" + 566 " (EQ (integralLT x y) |@true|)\n" + 567 " (< x y))))\n" + 568 "\n" + 569 "(BG_PUSH\n" + 570 " (FORALL (x y)\n" + 571 " (PATS (integralNE x y))\n" + 572 " (IFF\n" + 573 " (EQ (integralNE x y) |@true|)\n" + 574 " (NEQ x y))))\n" + 575 "\n" + 576 "(BG_PUSH\n" + 577 " (FORALL (x y)\n" + 578 " (PATS (refEQ x y))\n" + 579 " (IFF\n" + 580 " (EQ (refEQ x y) |@true|)\n" + 581 " (EQ x y))))\n" + 582 "\n" + 583 "(BG_PUSH\n" + 584 " (FORALL (x y)\n" + 585 " (PATS (refNE x y))\n" + 586 " (IFF\n" + 587 " (EQ (refNE x y) |@true|)\n" + 588 " (NEQ x y))))\n" + 589 "\n" + 590 "; === ESCJ 8: Section 5.3\n" + 591 "\n" + 592 "(BG_PUSH\n" + 593 " (FORALL (x y)\n" + 594 " (PATS (termConditional |@true| x y))\n" + 595 " (EQ (termConditional |@true| x y) x)))\n" + 596 "\n" + 597 "(BG_PUSH\n" + 598 " (FORALL (b x y)\n" + 599 " (PATS (termConditional b x y))\n" + 600 " (IMPLIES (NEQ b |@true|)\n" + 601 " (EQ (termConditional b x y) y))))\n" + 602 "\n" + 603 "; === Implementation of nonnullelements; not in ESCJ 8 (yet?):\n" + 604 "\n" + 605 "(DEFPRED (nonnullelements x e)\n" + 606 " (AND (NEQ x null)\n" + 607 " (FORALL (i)\n" + 608 " (IMPLIES (AND (<= 0 i)\n" + 609 " (< i (arrayLength x)))\n" + 610 " (NEQ (select (select e x) i) null)))))\n" + 611 "\n" + 612 "\n" + 613 "; === Axioms about classLiteral; not in ESCJ 8 (yet?):\n" + 614 "\n" + 615 "(BG_PUSH\n" + 616 " (FORALL (t)\n" + 617 " (PATS (classLiteral t))\n" + 618 " (AND (NEQ (classLiteral t) null)\n" + 619 " (is (classLiteral t) |T_java.lang.Class|)\n" + 620 " (isAllocated (classLiteral t) alloc))))\n" + 621 "\n" + 622 "(BG_PUSH\n" + 623 " (FORALL (t)\n" + 624 " (PATS (classLiteral t))\n" + 625 " (EQ (classLiteral t) t)\n" + 626 "))\n" + 627 "\n" + 628 "; === Axioms about properties of integral &, |, and /\n" + 629 "\n" + 630 "(BG_PUSH\n" + 631 " (FORALL (x y)\n" + 632 " (PATS (integralAnd x y))\n" + 633 " (IMPLIES\n" + 634 " (OR (<= 0 x) (<= 0 y))\n" + 635 " (<= 0 (integralAnd x y)))))\n" + 636 "\n" + 637 "(BG_PUSH\n" + 638 " (FORALL (x y)\n" + 639 " (PATS (integralAnd x y))\n" + 640 " (IMPLIES\n" + 641 " (<= 0 x)\n" + 642 " (<= (integralAnd x y) x))))\n" + 643 "\n" + 644 "(BG_PUSH\n" + 645 " (FORALL (x y)\n" + 646 " (PATS (integralAnd x y))\n" + 647 " (IMPLIES\n" + 648 " (<= 0 y)\n" + 649 " (<= (integralAnd x y) y))))\n" + 650 "\n" + 651 "(BG_PUSH\n" + 652 " (FORALL (x y)\n" + 653 " (PATS (integralOr x y))\n" + 654 " (IMPLIES\n" + 655 " (AND (<= 0 x) (<= 0 y))\n" + 656 " (AND (<= x (integralOr x y)) (<= y (integralOr x y))))))\n" + 657 "\n" + 658 "(BG_PUSH\n" + 659 " (FORALL (x y)\n" + 660 " (PATS (integralDiv x y))\n" + 661 " (IMPLIES\n" + 662 " (AND (<= 0 x) (< 0 y))\n" + 663 " (AND (<= 0 (integralDiv x y)) (<= (integralDiv x y) x)))))\n" + 664 "\n" + 665 "(BG_PUSH\n" + 666 " (FORALL (x y)\n" + 667 " (PATS (integralXor x y))\n" + 668 " (IMPLIES\n" + 669 " (AND (<= 0 x) (<= 0 y))\n" + 670 " (<= 0 (integralXor x y)))))\n" + 671 "\n" + 672 "(BG_PUSH\n" + 673 " (FORALL (n)\n" + 674 " (PATS (intShiftL 1 n))\n" + 675 " (IMPLIES\n" + 676 " (AND (<= 0 n) (< n 31))\n" + 677 " (<= 1 (intShiftL 1 n)))))\n" + 678 "\n" + 679 "(BG_PUSH\n" + 680 " (FORALL (n)\n" + 681 " (PATS (longShiftL 1 n))\n" + 682 " (IMPLIES\n" + 683 " (AND (<= 0 n) (< n 63))\n" + 684 " (<= 1 (longShiftL 1 n)))))\n" + 685 "\n" + 686 "; === A few floating point axioms - DRCok\n" + 687 ";; FIXME - floatingLT etc are predicates here, but are functions in ESC/java - is that a problem?\n" + 688 ";; FIXME - have to include NaN and infinity\n" + 689 "\n" + 690 ";; Order axioms\n" + 691 "(BG_PUSH\n" + 692 " (FORALL (d dd)\n" + 693 " (AND\n" + 694 " (OR\n" + 695 " (EQ |@true| (floatingLT d dd))\n" + 696 " (EQ |@true| (floatingEQ d dd))\n" + 697 " (EQ |@true| (floatingGT d dd))\n" + 698 " )\n" + 699 " (IFF (EQ |@true| (floatingLE d dd)) (OR (EQ |@true| (floatingEQ d dd)) (EQ |@true| (floatingLT d dd))))\n" + 700 " (IFF (EQ |@true| (floatingGE d dd)) (OR (EQ |@true| (floatingEQ d dd)) (EQ |@true| (floatingGT d dd))))\n" + 701 " (IFF (EQ |@true| (floatingLT d dd)) (EQ |@true| (floatingGT dd d)))\n" + 702 " (IFF (EQ |@true| (floatingLE d dd)) (EQ |@true| (floatingGE dd d)))\n" + 703 " (NOT (IFF (EQ |@true| (floatingLT d dd)) (EQ |@true| (floatingGE d dd))))\n" + 704 " (NOT (IFF (EQ |@true| (floatingGT d dd)) (EQ |@true| (floatingLE d dd))))\n" + 705 " )))\n" + 706 "\n" + 707 "\n" + 708 ";; floatingNE\n" + 709 "(BG_PUSH (FORALL (d dd) (IFF (EQ |@true| (floatingEQ d dd)) (NOT (EQ |@true| (floatingNE d dd)))) ))\n" + 710 "\n" + 711 ";; floatADD\n" + 712 "(BG_PUSH (FORALL (d dd)\n" + 713 " (IMPLIES (EQ |@true| (floatingGT d (floatingNEG dd))) (EQ |@true| (floatingGT (floatingADD d dd) |F_0.0|)))\n" + 714 "))\n" + 715 "\n" + 716 ";; floatMUL\n" + 717 ";;(BG_PUSH (FORALL (d dd) (AND\n" + 718 " ;;(IFF (OR (floatingEQ d |F_0.0|) (floatingEQ dd |F_0.0|)) (floatingEQ (floatingMUL d dd) |F_0.0|))\n" + 719 " ;;(IMPLIES (AND (floatingGT d |F_0.0|) (floatingGT dd |F_0.0|)) (floatingGT (floatingMUL d dd) |F_0.0|))\n" + 720 " ;;(IMPLIES (AND (floatingLT d |F_0.0|) (floatingLT dd |F_0.0|)) (floatingGT (floatingMUL d dd) |F_0.0|))\n" + 721 " ;;(IMPLIES (AND (floatingLT d |F_0.0|) (floatingGT dd |F_0.0|)) (floatingLT (floatingMUL d dd) |F_0.0|))\n" + 722 " ;;(IMPLIES (AND (floatingGT d |F_0.0|) (floatingLT dd |F_0.0|)) (floatingLT (floatingMUL d dd) |F_0.0|))\n" + 723 ";;)))\n" + 724 "\n" + 725 ";; floatingMOD\n" + 726 "(BG_PUSH\n" + 727 " (FORALL (d dd)\n" + 728 " (IMPLIES (EQ |@true| (floatingNE dd |F_0.0|)) (AND\n" + 729 " (IMPLIES (EQ |@true| (floatingGE d |F_0.0|)) (EQ |@true| (floatingGE (floatingMOD d dd) |F_0.0|)))\n" + 730 " (IMPLIES (EQ |@true| (floatingLE d |F_0.0|)) (EQ |@true| (floatingLE (floatingMOD d dd) |F_0.0|)))\n" + 731 "))))\n" + 732 "(BG_PUSH (FORALL (d dd) \n" + 733 " (IMPLIES (EQ |@true| (floatingGT dd |F_0.0|)) (AND\n" + 734 " (EQ |@true| (floatingGT (floatingMOD d dd) (floatingNEG dd))) \n" + 735 " (EQ |@true| (floatingLT (floatingMOD d dd) dd)) ))\n" + 736 "))\n" + 737 "(BG_PUSH (FORALL (d dd) \n" + 738 " (IMPLIES (EQ |@true| (floatingLT dd |F_0.0|)) (EQ |@true| (floatingLT (floatingMOD d dd) (floatingNEG dd)))) ))\n" + 739 "(BG_PUSH (FORALL (d dd) \n" + 740 " (IMPLIES (EQ |@true| (floatingLT dd |F_0.0|)) (EQ |@true| (floatingGT (floatingMOD d dd) dd))) ))\n" + 741 "\n" + 742 "; === Temporary kludge to speed up distinguishing small integers:\n" + 743 "\n" + 744 "(BG_PUSH\n" + 745 " (DISTINCT -10 -9 -8 -7 -6 -5 -4 -3 -2 -1 0 1 2 3 4 5 6 7 8 9\n" + 746 " 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29\n" + 747 " 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49\n" + 748 " 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69\n" + 749 " 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89\n" + 750 " 90 91 92 93 94 95 96 97 98 99\n" + 751 " 100 101 102 103 104 105 106 107 108 109\n" + 752 " 110 111 112 113 114 115 116 117 118 119\n" + 753 " 120 121 122 123 124 125 126 127 128 129\n" + 754 " 130 131 132 133 134 135 136 137 138 139\n" + 755 " 140 141 142 143 144 145 146 147 148 149\n" + 756 " 150 151 152 153 154 155 156 157 158 159\n" + 757 " 160 161 162 163 164 165 166 167 168 169\n" + 758 " 170 171 172 173 174 175 176 177 178 179\n" + 759 " 180 181 182 183 184 185 186 187 188 189\n" + 760 " 190 191 192 193 194 195 196 197 198 199\n" + 761 " 200 201 202 203 204 205 206 207 208 209\n" + 762 " 210 211 212 213 214 215 216 217 218 219\n" + 763 " 220 221 222 223 224 225 226 227 228 229\n" + 764 " 230 231 232 233 234 235 236 237 238 239\n" + 765 " 240 241 242 243 244 245 246 247 248 249\n" + 766 " 250 251 252 253 254 255 256 257 258 259\n" + 767 " 260 261 262 263 264 265 266 267 268 269\n" + 768 " 270 271 272 273 274 275 276 277 278 279\n" + 769 " 280 281 282 283 284 285 286 287 288 289\n" + 770 " 290 291 292 293 294 295 296 297 298 299\n" + 771 " 300 301 302 303 304 305 306 307 308 309\n" + 772 " 310 311 312 313 314 315 316 317 318 319\n" + 773 " 320 321 322 323 324 325 326 327 328 329\n" + 774 " 330 331 332 333 334 335 336 337 338 339\n" + 775 " 340 341 342 343 344 345 346 347 348 349\n" + 776 " 350 351 352 353 354 355 356 357 358 359\n" + 777 " 360 361 362 363 364 365 366 367 368 369\n" + 778 " 370 371 372 373 374 375 376 377 378 379\n" + 779 " 380 381 382 383 384 385 386 387 388 389\n" + 780 " 390 391 392 393 394 395 396 397 398 399))\n" + 781 "\n" + 782 ";----------------------------------------------------------------------\n" + 783 "; End of Universal background predicate\n" + 784 ";----------------------------------------------------------------------\n" + 785 "(PROMPT_ON)\n" + 786 ""; 787 }