/[eiffelstudio]/branches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl
ViewVC logotype

Contents of /branches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93378 - (show annotations)
Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File size: 20724 byte(s)
AutoProof: continued ownership implementation.

1 // ----------------------------------------------------------------------
2 // Sets
3
4 type Set T = [T]bool;
5
6 function Set#Empty<T>(): Set T;
7 axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
8
9 function Set#Singleton<T>(T): Set T;
10 axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
11 axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
12
13 function Set#UnionOne<T>(Set T, T): Set T;
14 axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
15 Set#UnionOne(a,x)[o] <==> o == x || a[o]);
16 axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
17 Set#UnionOne(a, x)[x]);
18 axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
19 a[y] ==> Set#UnionOne(a, x)[y]);
20
21 function Set#Union<T>(Set T, Set T): Set T;
22 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
23 Set#Union(a,b)[o] <==> a[o] || b[o]);
24 axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }
25 a[y] ==> Set#Union(a, b)[y]);
26 axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), b[y] }
27 b[y] ==> Set#Union(a, b)[y]);
28 axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
29 Set#Disjoint(a, b) ==>
30 Set#Difference(Set#Union(a, b), a) == b &&
31 Set#Difference(Set#Union(a, b), b) == a);
32
33 function Set#Intersection<T>(Set T, Set T): Set T;
34 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
35 Set#Intersection(a,b)[o] <==> a[o] && b[o]);
36
37 axiom (forall<T> a, b: Set T :: { Set#Union(Set#Union(a, b), b) }
38 Set#Union(Set#Union(a, b), b) == Set#Union(a, b));
39 axiom (forall<T> a, b: Set T :: { Set#Union(a, Set#Union(a, b)) }
40 Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));
41 axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }
42 Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));
43 axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }
44 Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
45
46 function Set#Difference<T>(Set T, Set T): Set T;
47 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }
48 Set#Difference(a,b)[o] <==> a[o] && !b[o]);
49 axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
50 b[y] ==> !Set#Difference(a, b)[y] );
51
52 function Set#Subset<T>(Set T, Set T): bool;
53 axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
54 Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));
55
56 function Set#Equal<T>(Set T, Set T): bool;
57 axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }
58 Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));
59 axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets
60 Set#Equal(a,b) ==> a == b);
61
62 function Set#Disjoint<T>(Set T, Set T): bool;
63 axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }
64 Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
65
66 // ----------------------------------------------------------------------
67 // Reference types
68
69 type ref; // Type definition for reference types
70 const Void: ref; // Constant for Void references
71
72 // ----------------------------------------------------------------------
73 // Heap and allocation
74
75 type Field _; // Type of a field (with open subtype)
76 function IsGhostField<alpha>(field: Field alpha): bool; // Is this field a ghost field?
77
78 type HeapType = <alpha>[ref, Field alpha]alpha; // Type of a heap (with generic field subtype and generic content type)
79 const unique allocated: Field bool; // Ghost field for allocation status of objects
80
81 // Function which defines basic properties of a heap
82 function IsHeap(heap: HeapType): bool {
83 true
84 }
85
86 // The global heap (which is always a heap)
87 var Heap: HeapType where IsHeap(Heap);
88
89 // ----------------------------------------------------------------------
90 // Typing
91
92 type Type; // Type definition for Eiffel types
93 const unique ANY: Type; // Type for ANY
94 const unique NONE: Type; // Type for NONE
95
96 // Type for generics
97 const unique G1: Type;
98 const unique G2: Type;
99 const unique G3: Type;
100 const unique G4: Type;
101 const unique G5: Type;
102 const unique G6: Type;
103 const unique G7: Type;
104 const unique G8: Type;
105 const unique G9: Type;
106
107 // Type function for objects.
108 function type_of(o: ref) returns (Type);
109 function is_frozen(t: Type) returns (bool);
110
111 // Typing axioms
112 axiom (forall t: Type :: t <: ANY); // All types inherit from ANY.
113 axiom (forall t: Type :: NONE <: t); // NONE inherits from all types.
114 axiom (forall h: HeapType :: h[Void, allocated]); // Void is always allocated.
115 axiom (forall h: HeapType, f: Field ref, o: ref :: h[o, allocated] ==> h[h[o, f], allocated]); // All reference fields are allocated.
116 axiom (forall r: ref :: (r == Void) <==> (type_of(r) == NONE)); // Void is only reference of type NONE.
117 axiom (forall a, b: ref :: (type_of(a) != type_of(b)) ==> (a != b)); // Objects that have different dynamic type cannot be aliased.
118 axiom (forall t: Type :: is_frozen(t) ==> (forall t2: Type :: t2 <: t ==> t2 == NONE)); // Only NONE inherits from frozen types.
119 axiom (forall t: Type, r: ref :: (r != Void && type_of(r) <: t && is_frozen(t)) ==> (type_of(r) == t)); // Non-void references of a frozen type are exact.
120
121 function ANY.self_inv(heap: HeapType, current: ref) returns (bool) {
122 true
123 }
124
125 function NONE.self_inv(heap: HeapType, current: ref) returns (bool) {
126 false
127 }
128
129 // ----------------------------------------------------------------------
130 // Ownership
131
132 var Writes: Set ref; // Set of all currently writable objects
133
134 const unique closed: Field bool; // Ghost field for open/closed status of an object.
135 const unique owner: Field ref; // Ghost field for owner of an object.
136 const unique owns: Field (Set ref); // Ghost field for owns set of an object.
137 const unique observers: Field (Set ref); // Ghost field for observers set of an object.
138 const unique subjects: Field (Set ref); // Ghost field for subjects set of an object.
139
140 // Is o free? (owner is open)
141 function {:inline} is_free(h: HeapType, o: ref): bool {
142 h[o, owner] == Void
143 }
144
145 // Is o wrapped in h? (closed and free)
146 function {:inline} is_wrapped(h: HeapType, o: ref): bool {
147 h[o, closed] && is_free(h, o)
148 }
149
150 // Is o open in h? (not closed and free)
151 function {:inline} is_open(h: HeapType, o: ref): bool {
152 !h[o, closed]
153 }
154
155 // Is o closed in h?
156 function {:inline} is_closed(h: HeapType, o: ref): bool {
157 h[o, closed]
158 }
159
160 // Only allocated references can be in ghost sets
161 axiom (forall h: HeapType, o: ref, r: ref :: h[o, observers][r] ==> h[r, allocated]);
162 axiom (forall h: HeapType, o: ref, r: ref :: h[o, owns][r] ==> h[r, allocated]);
163 axiom (forall h: HeapType, o: ref, r: ref :: h[o, subjects][r] ==> h[r, allocated]);
164
165 // Is o' in the ownership domain of o? Yes if they are equal, or both closed and o' is transitively owned by o
166 function in_domain(h: HeapType, o: ref, o': ref): bool
167 {
168 o == o' ||
169 (
170 h[o, closed] &&
171 h[o', closed] &&
172 in_domain(h, o, h[o', owner])
173 )
174 }
175
176 axiom (forall h: HeapType, o, o': ref :: { in_domain(h, o, o') } h[o, closed] && h[o, owns][o'] ==> in_domain(h, o, o'));
177
178 // Objects outside of ownership domains of mods did not change, unless they were newly allocated
179 function writes(h: HeapType, h': HeapType, mods: Set ref): bool {
180 (forall <T> o: ref, f: Field T :: { h[o, f] } { h'[o, f] }
181 ((forall o': ref :: { mods[o'] } { in_domain(h, o', o) } mods[o'] ==> !in_domain(h, o', o)) &&
182 h[o, allocated])
183 ==>
184 h'[o, f] == h[o, f])
185 &&
186 no_garbage(h, h')
187 }
188
189 // The allocation status of objects does not change
190 function no_garbage(old_heap: HeapType, new_heap: HeapType): bool {
191 (forall o: ref :: { new_heap[o, allocated] } { old_heap[o, allocated] }
192 old_heap[o, allocated] ==> new_heap[o, allocated])
193 }
194
195 // Objects that:
196 // 1. were in the writes set and have not been captured by the routine
197 // 2. have been released by the routine
198 // 3. newly allocated and not captured
199 // are still writable
200 function writes_changed(h: HeapType, h': HeapType, wr: Set ref, wr': Set ref): bool
201 {
202 (forall o: ref ::
203 (wr[o] && is_free(h', o)) ||
204 (!is_free(h, o) && is_free(h', o)) ||
205 (!h[o, allocated] && h'[o, allocated] && is_free(h', o))
206 ==>
207 wr'[o])
208 }
209
210 // Is invariant of object o satisifed?
211 function user_inv(h: HeapType, o: ref): bool;
212
213 // Is object o closed or the invariant satisfied?
214 function inv(h: HeapType, o: ref): bool {
215 h[o, closed] ==> user_inv(h, o)
216 }
217
218 // Invariant of None is false
219 // axiom (forall h: HeapType, o: ref :: type_of(o) == NONE ==> !user_inv(h, o));
220
221 // Global heap invariants
222 function {:inline true} global_heap(h: HeapType): bool
223 {
224 is_open(h, Void) && // G1
225 (forall o: ref :: h[o, allocated] && is_free(h, o) ==> (h[o, owner] == Void)) && // G2
226 (forall o: ref :: h[o, allocated] && is_open(h, o) ==> is_free(h, o)) && // G3
227 (forall o: ref, o': ref :: h[o, allocated] && h[o', allocated] && h[o, closed] && h[o, owns][o'] ==> (h[o', closed] && h[o', owner] == o)) && // G4
228 (forall o: ref :: h[o, allocated] && h[o, closed] ==> inv(h, o)) // G5
229 }
230
231 // Global invariants
232 function {:inline true} global(h: HeapType, wr: Set ref): bool
233 {
234 global_heap(h) &&
235 (forall o: ref :: wr[o] ==> h[o, allocated] && is_free(h, o))
236 }
237
238 // Allocate fresh object
239 procedure allocate(t: Type) returns (result: ref);
240 modifies Heap, Writes;
241 ensures !old(Heap[result, allocated]); // AL1
242 ensures Heap[result, allocated]; // AL2
243 ensures result != Void;
244 ensures type_of(result) == t;
245 ensures is_open(Heap, result); // AL3
246 ensures is_free(Heap, result); // AL4
247 ensures Set#Equal(Heap[result, owns], Set#Empty());
248 ensures Set#Equal(Heap[result, observers], Set#Empty());
249 ensures Set#Equal(Heap[result, subjects], Set#Empty());
250 ensures Writes == old(Set#UnionOne(Writes, result));
251 ensures (forall <T> o: ref, f: Field T :: o != result ==> Heap[o, f] == old(Heap[o, f]));
252
253 // Update Heap position Current.field with value.
254 procedure update_heap<T>(Current: ref, field: Field T, value: T);
255 requires field != closed && field != owner; // update tag:closed_or_owner_not_allowed UP4
256 requires is_open(Heap, Current); // update tag:target_open UP1
257 requires (forall o: ref :: Heap[Current, observers][o] ==> is_open(Heap, o)); // update tag:all_observers_open UP2
258 requires Writes[Current]; // update tag:target_writable UP3
259 modifies Heap;
260 ensures Heap[Current, field] == value;
261 ensures (forall<U> o: ref, f: Field U :: !(o == Current && f == field) ==> Heap[o, f] == old(Heap[o, f]));
262
263 // Unwrap o
264 procedure unwrap(o: ref);
265 requires is_wrapped(Heap, o); // pre tag:wrapped UW1
266 requires Writes[o]; // pre tag:writable UW2
267 modifies Heap, Writes;
268 ensures is_open(Heap, o); // UWE1
269 ensures (forall o': ref :: old(Heap[o, owns][o']) ==> is_wrapped(Heap, o')); // UWE2
270 ensures Set#Equal(Writes, old(Set#Union(Writes, Heap[o, owns]))); // UWE3
271 ensures (forall <T> o': ref, f: Field T :: !(o' == o && f == closed) && !(old(Heap[o, owns][o']) && f == owner) ==> Heap[o', f] == old(Heap[o', f]));
272 ensures user_inv(Heap, o);
273
274 procedure unwrap_all (Current: ref, s: Set ref);
275 requires (forall o: ref :: s[o] ==> is_wrapped(Heap, o)); // pre tag:wrapped UW1
276 requires (forall o: ref :: s[o] ==> Writes[o]); // pre tag:writable UW2
277 modifies Heap, Writes;
278 ensures (forall o: ref :: s[o] ==> is_open(Heap, o)); // UWE1
279 ensures (forall o: ref :: s[o] ==> (forall o': ref :: old(Heap[o, owns][o']) ==> is_wrapped(Heap, o'))); // UWE2
280 ensures (forall o: ref :: s[o] ==> Set#Subset(old(Heap[o, owns]), Writes)) && Set#Subset(old(Writes), Writes); // ensures Set#Equal(Writes, old(Set#Union(Writes, Heap[o, owns]))); // UWE3
281 ensures (forall <T> o: ref, f: Field T :: !(s[o] && f == closed) && !((exists o': ref :: s[o'] && old(Heap[o', owns][o])) && f == owner) ==> Heap[o, f] == old(Heap[o, f]));
282 ensures (forall o: ref :: s[o] ==> user_inv(Heap, o));
283
284 // Wrap o
285 procedure wrap(o: ref);
286 requires is_open(Heap, o); // pre tag:open W1
287 requires user_inv(Heap, o); // pre tag:invariant_holds W2
288 requires (forall o': ref :: Heap[o, owns][o'] ==> is_wrapped(Heap, o') && Writes[o']); // pre tag:owned_objects_wrapped W3
289 requires Writes[o]; // pre tag:writable W4
290 modifies Heap, Writes;
291 ensures Set#Equal(Writes, old(Set#Difference(Writes, Heap[o, owns]))); // WE1
292 ensures (forall o': ref :: old(Heap[o, owns][o']) ==> Heap[o', owner] == o); // WE2
293 ensures is_wrapped(Heap, o); // WE3
294 ensures (forall <T> o': ref, f: Field T :: !(o' == o && f == closed) && !(old(Heap[o, owns][o']) && f == owner) ==> Heap[o', f] == old(Heap[o', f]));
295
296 procedure wrap_all(Current: ref, s: Set ref);
297 requires (forall o: ref :: s[o] ==> is_open(Heap, o)); // pre tag:open W1
298 requires (forall o: ref :: s[o] ==> user_inv(Heap, o)); // pre tag:invariant_holds W2
299 requires (forall o: ref :: s[o] ==> (forall o': ref :: Heap[o, owns][o'] ==> is_wrapped(Heap, o'))); // pre tag:owned_objects_wrapped W3
300 requires (forall o: ref :: s[o] ==> (forall o': ref :: Heap[o, owns][o'] ==> Writes[o'])); // pre tag:owned_objects_writable W3
301 requires (forall o: ref :: s[o] ==> Writes[o]); // pre tag:writable W4
302 modifies Heap, Writes;
303 ensures (forall o, o': ref :: s[o] && Heap[o, owns][o'] ==> !Writes[o']); // ensures Set#Equal(Writes, old(Set#Difference(Writes, Heap[o, owns]))); // WE1
304 ensures (forall o, o': ref :: old(Writes[o']) && (!s[o] || !Heap[o, owns][o']) ==> Writes[o']); // ensures Set#Equal(Writes, old(Set#Difference(Writes, Heap[o, owns]))); // WE1
305 ensures (forall o: ref :: s[o] ==> (forall o': ref :: old(Heap[o, owns][o']) ==> Heap[o', owner] == o)); // WE2
306 ensures (forall o: ref :: s[o] ==> is_wrapped(Heap, o)); // WE3
307 ensures (forall <T> o: ref, f: Field T :: !(s[o] && f == closed) && !((exists o': ref :: s[o'] && old(Heap[o', owns][o])) && f == owner) ==> Heap[o, f] == old(Heap[o, f]));
308
309 // ----------------------------------------------------------------------
310 // Attached/Detachable functions
311
312 // Property that reference `o' is attached to an object of type `t' on heap `heap'.
313 function attached_exact(heap: HeapType, o: ref, t: Type) returns (bool) {
314 (o != Void) && (heap[o, allocated]) && (type_of(o) == t)
315 }
316
317 // Property that reference `o' is attached and conforms to type `t' on heap `heap'.
318 function attached(heap: HeapType, o: ref, t: Type) returns (bool) {
319 (o != Void) && (heap[o, allocated]) && (type_of(o) == t)
320
321 // ******************* reenable when ownership and inheritance are combined *******************
322 // (o != Void) && (heap[o, allocated]) && (type_of(o) <: t)
323
324 }
325
326 // Property that reference `o' is either Void or attached and conforms to `t' on heap `heap'.
327 function detachable(heap: HeapType, o: ref, t: Type) returns (bool) {
328 (o == Void) || (attached(heap, o, t))
329 }
330
331 // Property that field `f' is of attached type `t'.
332 function attached_attribute(heap: HeapType, o: ref, f: Field ref, t: Type) returns (bool) {
333 (o != Void) && (heap[o, allocated]) ==> attached(heap, heap[o, f], t)
334 }
335
336 // Property that field `f' is of detachable type `t'.
337 function detachable_attribute(heap: HeapType, o: ref, f: Field ref, t: Type) returns (bool) {
338 (o != Void) && (heap[o, allocated]) ==> detachable(heap, heap[o, f], t)
339 }
340
341 // ----------------------------------------------------------------------
342 // Basic types
343
344 // Integer boxing
345
346 const unique INTEGER: Type;
347
348 function boxed_int(i: int) returns (ref);
349 function unboxed_int(r: ref) returns (int);
350
351 axiom (forall i: int :: unboxed_int(boxed_int(i)) == i);
352 axiom (forall i1, i2: int :: (i1 == i2) ==> (boxed_int(i1) == boxed_int(i2)));
353 axiom (forall i: int :: boxed_int(i) != Void && type_of(boxed_int(i)) == INTEGER);
354 axiom (forall heap: HeapType, i: int :: heap[boxed_int(i), allocated]);
355
356
357 // Boolean boxing
358
359 const unique BOOLEAN: Type;
360 const unique boxed_true: ref;
361 const unique boxed_false: ref;
362
363 function boxed_bool(b: bool) returns (ref);
364 function unboxed_bool(r: ref) returns (bool);
365
366 axiom (boxed_bool(true) == boxed_true);
367 axiom (boxed_bool(false) == boxed_false);
368 axiom (unboxed_bool(boxed_true) == true);
369 axiom (unboxed_bool(boxed_false) == false);
370 axiom (boxed_true != boxed_false);
371 axiom (boxed_true != Void && type_of(boxed_true) == BOOLEAN);
372 axiom (boxed_false != Void && type_of(boxed_false) == BOOLEAN);
373 axiom (forall heap: HeapType :: heap[boxed_true, allocated]);
374 axiom (forall heap: HeapType :: heap[boxed_false, allocated]);
375
376 // Bounded integers
377
378 function is_integer_8(i: int) returns (bool) {
379 (-128 <= i) && (i <= 127)
380 }
381 function is_integer_16(i: int) returns (bool) {
382 (-32768 <= i) && (i <= 32767)
383 }
384 function is_integer_32(i: int) returns (bool) {
385 (-2147483648 <= i) && (i <= 2147483647)
386 }
387 function is_integer_64(i: int) returns (bool) {
388 (-9223372036854775808 <= i) && (i <= 9223372036854775807)
389 }
390 function is_natural(i: int) returns (bool) {
391 (0 <= i)
392 }
393 function is_natural_8(i: int) returns (bool) {
394 (0 <= i) && (i <= 255)
395 }
396 function is_natural_16(i: int) returns (bool) {
397 (0 <= i) && (i <= 65535)
398 }
399 function is_natural_32(i: int) returns (bool) {
400 (0 <= i) && (i <= 4294967295)
401 }
402 function is_natural_64(i: int) returns (bool) {
403 (0 <= i) && (i <= 18446744073709551615)
404 }
405
406 // Numeric conversions
407
408 function int_to_integer_8(i: int) returns (int);
409 axiom (forall i: int :: { int_to_integer_8(i) } is_integer_8(i) ==> int_to_integer_8(i) == i);
410 axiom (forall i: int :: { int_to_integer_8(i) } is_integer_8(int_to_integer_8(i)));
411
412 function int_to_integer_16(i: int) returns (int);
413 axiom (forall i: int :: { int_to_integer_16(i) } is_integer_16(i) ==> int_to_integer_16(i) == i);
414 axiom (forall i: int :: { int_to_integer_16(i) } is_integer_16(int_to_integer_16(i)));
415
416 function int_to_integer_32(i: int) returns (int);
417 axiom (forall i: int :: { int_to_integer_32(i) } is_integer_32(i) ==> int_to_integer_32(i) == i);
418 axiom (forall i: int :: { int_to_integer_32(i) } is_integer_32(int_to_integer_32(i)));
419
420 function int_to_integer_64(i: int) returns (int);
421 axiom (forall i: int :: { int_to_integer_64(i) } is_integer_64(i) ==> int_to_integer_64(i) == i);
422 axiom (forall i: int :: { int_to_integer_64(i) } is_integer_64(int_to_integer_64(i)));
423
424 function int_to_natural_8(i: int) returns (int);
425 axiom (forall i: int :: { int_to_natural_8(i) } is_natural_8(i) ==> int_to_natural_8(i) == i);
426 axiom (forall i: int :: { int_to_natural_8(i) } is_natural_8(int_to_natural_8(i)));
427
428 function int_to_natural_16(i: int) returns (int);
429 axiom (forall i: int :: { int_to_natural_16(i) } is_natural_16(i) ==> int_to_natural_16(i) == i);
430 axiom (forall i: int :: { int_to_natural_16(i) } is_natural_16(int_to_natural_16(i)));
431
432 function int_to_natural_32(i: int) returns (int);
433 axiom (forall i: int :: { int_to_natural_32(i) } is_natural_32(i) ==> int_to_natural_32(i) == i);
434 axiom (forall i: int :: { int_to_natural_32(i) } is_natural_32(int_to_natural_32(i)));
435
436 function int_to_natural_64(i: int) returns (int);
437 axiom (forall i: int :: { int_to_natural_64(i) } is_natural_64(i) ==> int_to_natural_64(i) == i);
438 axiom (forall i: int :: { int_to_natural_64(i) } is_natural_64(int_to_natural_64(i)));
439
440 function real_to_integer_32(r: real) returns (int);
441 axiom (forall r: real :: { real_to_integer_32(r) } is_integer_32(int(r)) ==> real_to_integer_32(r) == int(r));
442 axiom (forall r: real :: { real_to_integer_32(r) } (!is_integer_32(int(r)) && r < 0.0) ==> real_to_integer_32(r) == -2147483648);
443 axiom (forall r: real :: { real_to_integer_32(r) } (!is_integer_32(int(r)) && r > 0.0) ==> real_to_integer_32(r) == 2147483647);
444
445 function real_to_integer_64(r: real) returns (int);
446 axiom (forall r: real :: { real_to_integer_64(r) } is_integer_64(int(r)) ==> real_to_integer_64(r) == int(r));
447 axiom (forall r: real :: { real_to_integer_64(r) } (!is_integer_64(int(r)) && r < 0.0) ==> real_to_integer_64(r) == -9223372036854775808);
448 axiom (forall r: real :: { real_to_integer_64(r) } (!is_integer_64(int(r)) && r > 0.0) ==> real_to_integer_64(r) == 9223372036854775807);
449
450 // Arithmetic functions
451
452 function add(a, b: int): int { a + b }
453 function subtract(a, b: int): int { a - b }
454 function multiply(a, b: int): int { a * b }
455 function modulo(a, b: int): int { a mod b }
456 function divide(a, b: int): int { a div b }
457
458 // Expanded types
459
460 type unknown;
461
462 // Address operator
463
464 function address(a: ref) returns (int);
465 axiom (forall a, b: ref :: (a != b) <==> (address(a) != address(b))); // Different objects have different heap addresses.
466 axiom (forall a: ref :: is_integer_64(address(a))); // Addresses are 64 bit integers.
467

  ViewVC Help
Powered by ViewVC 1.1.23