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