45044
|
1 |
/*********************************************************/
|
|
2 |
/*Proof Rule Declarations*/
|
|
3 |
/*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
|
|
4 |
/*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
|
|
5 |
/*********************************************************/
|
|
6 |
|
|
7 |
|
|
8 |
/*DATE : 22-SEP-2011 11:10:52.42*/
|
|
9 |
|
|
10 |
/*procedure Complex_Types_App.Initialize*/
|
|
11 |
|
|
12 |
|
|
13 |
rule_family initialize_rules:
|
|
14 |
X requires [X:any] &
|
|
15 |
X <= Y requires [X:ire, Y:ire] &
|
|
16 |
X >= Y requires [X:ire, Y:ire].
|
|
17 |
|
|
18 |
initialize_rules(1): integer__size >= 0 may_be_deduced.
|
|
19 |
initialize_rules(2): integer__first may_be_replaced_by -2147483648.
|
|
20 |
initialize_rules(3): integer__last may_be_replaced_by 2147483647.
|
|
21 |
initialize_rules(4): integer__base__first may_be_replaced_by -2147483648.
|
|
22 |
initialize_rules(5): integer__base__last may_be_replaced_by 2147483647.
|
|
23 |
initialize_rules(6): complex_types__day__size >= 0 may_be_deduced.
|
|
24 |
initialize_rules(7): complex_types__day__first may_be_replaced_by complex_types__mon.
|
|
25 |
initialize_rules(8): complex_types__day__last may_be_replaced_by complex_types__sun.
|
|
26 |
initialize_rules(9): complex_types__day__base__first may_be_replaced_by complex_types__mon.
|
|
27 |
initialize_rules(10): complex_types__day__base__last may_be_replaced_by complex_types__sun.
|
|
28 |
initialize_rules(11): complex_types__day__pos(complex_types__day__first) may_be_replaced_by 0.
|
|
29 |
initialize_rules(12): complex_types__day__pos(complex_types__mon) may_be_replaced_by 0.
|
|
30 |
initialize_rules(13): complex_types__day__val(0) may_be_replaced_by
|
|
31 |
complex_types__mon.
|
|
32 |
initialize_rules(14): complex_types__day__pos(complex_types__tue) may_be_replaced_by 1.
|
|
33 |
initialize_rules(15): complex_types__day__val(1) may_be_replaced_by
|
|
34 |
complex_types__tue.
|
|
35 |
initialize_rules(16): complex_types__day__pos(complex_types__wed) may_be_replaced_by 2.
|
|
36 |
initialize_rules(17): complex_types__day__val(2) may_be_replaced_by
|
|
37 |
complex_types__wed.
|
|
38 |
initialize_rules(18): complex_types__day__pos(complex_types__thu) may_be_replaced_by 3.
|
|
39 |
initialize_rules(19): complex_types__day__val(3) may_be_replaced_by
|
|
40 |
complex_types__thu.
|
|
41 |
initialize_rules(20): complex_types__day__pos(complex_types__fri) may_be_replaced_by 4.
|
|
42 |
initialize_rules(21): complex_types__day__val(4) may_be_replaced_by
|
|
43 |
complex_types__fri.
|
|
44 |
initialize_rules(22): complex_types__day__pos(complex_types__sat) may_be_replaced_by 5.
|
|
45 |
initialize_rules(23): complex_types__day__val(5) may_be_replaced_by
|
|
46 |
complex_types__sat.
|
|
47 |
initialize_rules(24): complex_types__day__pos(complex_types__sun) may_be_replaced_by 6.
|
|
48 |
initialize_rules(25): complex_types__day__val(6) may_be_replaced_by
|
|
49 |
complex_types__sun.
|
|
50 |
initialize_rules(26): complex_types__day__pos(complex_types__day__last) may_be_replaced_by 6.
|
|
51 |
initialize_rules(27): complex_types__day__pos(succ(X)) may_be_replaced_by
|
|
52 |
complex_types__day__pos(X) + 1
|
|
53 |
if [X <=complex_types__sun, X <> complex_types__sun].
|
|
54 |
initialize_rules(28): complex_types__day__pos(pred(X)) may_be_replaced_by
|
|
55 |
complex_types__day__pos(X) - 1
|
|
56 |
if [X >=complex_types__mon, X <> complex_types__mon].
|
|
57 |
initialize_rules(29): complex_types__day__pos(X) >= 0 may_be_deduced_from
|
|
58 |
[complex_types__mon <= X, X <= complex_types__sun].
|
|
59 |
initialize_rules(30): complex_types__day__pos(X) <= 6 may_be_deduced_from
|
|
60 |
[complex_types__mon <= X, X <= complex_types__sun].
|
|
61 |
initialize_rules(31): complex_types__day__val(X) >=
|
|
62 |
complex_types__mon may_be_deduced_from
|
|
63 |
[0 <= X, X <= 6].
|
|
64 |
initialize_rules(32): complex_types__day__val(X) <=
|
|
65 |
complex_types__sun may_be_deduced_from
|
|
66 |
[0 <= X, X <= 6].
|
|
67 |
initialize_rules(33): succ(complex_types__day__val(X)) may_be_replaced_by
|
|
68 |
complex_types__day__val(X+1)
|
|
69 |
if [0 <= X, X < 6].
|
|
70 |
initialize_rules(34): pred(complex_types__day__val(X)) may_be_replaced_by
|
|
71 |
complex_types__day__val(X-1)
|
|
72 |
if [0 < X, X <= 6].
|
|
73 |
initialize_rules(35): complex_types__day__pos(complex_types__day__val(X)) may_be_replaced_by X
|
|
74 |
if [0 <= X, X <= 6].
|
|
75 |
initialize_rules(36): complex_types__day__val(complex_types__day__pos(X)) may_be_replaced_by X
|
|
76 |
if [complex_types__mon <= X, X <= complex_types__sun].
|
|
77 |
initialize_rules(37): complex_types__day__pos(X) <=
|
|
78 |
complex_types__day__pos(Y) & X <= Y are_interchangeable
|
|
79 |
if [complex_types__mon <= X, X <= complex_types__sun,
|
|
80 |
complex_types__mon <= Y, Y <= complex_types__sun].
|
|
81 |
initialize_rules(38): complex_types__day__val(X) <=
|
|
82 |
complex_types__day__val(Y) & X <= Y are_interchangeable
|
|
83 |
if [0 <= X, X <= 6, 0 <= Y, Y <= 6].
|
|
84 |
initialize_rules(39): complex_types__array_index__size >= 0 may_be_deduced.
|
|
85 |
initialize_rules(40): complex_types__array_index__first may_be_replaced_by 0.
|
|
86 |
initialize_rules(41): complex_types__array_index__last may_be_replaced_by 9.
|
|
87 |
initialize_rules(42): complex_types__array_index__base__first may_be_replaced_by -2147483648.
|
|
88 |
initialize_rules(43): complex_types__array_index__base__last may_be_replaced_by 2147483647.
|
|
89 |
initialize_rules(44): complex_types__record_type__size >= 0 may_be_deduced.
|
|
90 |
initialize_rules(45): A = B may_be_deduced_from
|
|
91 |
[goal(checktype(A,complex_types__record_type)),
|
|
92 |
goal(checktype(B,complex_types__record_type)),
|
|
93 |
fld_field1(A) = fld_field1(B),
|
|
94 |
fld_field2(A) = fld_field2(B)].
|