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

  ViewVC Help
Powered by ViewVC 1.1.23