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    }