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 13rule_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 18initialize_rules(1): integer__size >= 0 may_be_deduced. 19initialize_rules(2): integer__first may_be_replaced_by -2147483648. 20initialize_rules(3): integer__last may_be_replaced_by 2147483647. 21initialize_rules(4): integer__base__first may_be_replaced_by -2147483648. 22initialize_rules(5): integer__base__last may_be_replaced_by 2147483647. 23initialize_rules(6): complex_types__day__size >= 0 may_be_deduced. 24initialize_rules(7): complex_types__day__first may_be_replaced_by complex_types__mon. 25initialize_rules(8): complex_types__day__last may_be_replaced_by complex_types__sun. 26initialize_rules(9): complex_types__day__base__first may_be_replaced_by complex_types__mon. 27initialize_rules(10): complex_types__day__base__last may_be_replaced_by complex_types__sun. 28initialize_rules(11): complex_types__day__pos(complex_types__day__first) may_be_replaced_by 0. 29initialize_rules(12): complex_types__day__pos(complex_types__mon) may_be_replaced_by 0. 30initialize_rules(13): complex_types__day__val(0) may_be_replaced_by 31 complex_types__mon. 32initialize_rules(14): complex_types__day__pos(complex_types__tue) may_be_replaced_by 1. 33initialize_rules(15): complex_types__day__val(1) may_be_replaced_by 34 complex_types__tue. 35initialize_rules(16): complex_types__day__pos(complex_types__wed) may_be_replaced_by 2. 36initialize_rules(17): complex_types__day__val(2) may_be_replaced_by 37 complex_types__wed. 38initialize_rules(18): complex_types__day__pos(complex_types__thu) may_be_replaced_by 3. 39initialize_rules(19): complex_types__day__val(3) may_be_replaced_by 40 complex_types__thu. 41initialize_rules(20): complex_types__day__pos(complex_types__fri) may_be_replaced_by 4. 42initialize_rules(21): complex_types__day__val(4) may_be_replaced_by 43 complex_types__fri. 44initialize_rules(22): complex_types__day__pos(complex_types__sat) may_be_replaced_by 5. 45initialize_rules(23): complex_types__day__val(5) may_be_replaced_by 46 complex_types__sat. 47initialize_rules(24): complex_types__day__pos(complex_types__sun) may_be_replaced_by 6. 48initialize_rules(25): complex_types__day__val(6) may_be_replaced_by 49 complex_types__sun. 50initialize_rules(26): complex_types__day__pos(complex_types__day__last) may_be_replaced_by 6. 51initialize_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]. 54initialize_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]. 57initialize_rules(29): complex_types__day__pos(X) >= 0 may_be_deduced_from 58 [complex_types__mon <= X, X <= complex_types__sun]. 59initialize_rules(30): complex_types__day__pos(X) <= 6 may_be_deduced_from 60 [complex_types__mon <= X, X <= complex_types__sun]. 61initialize_rules(31): complex_types__day__val(X) >= 62 complex_types__mon may_be_deduced_from 63 [0 <= X, X <= 6]. 64initialize_rules(32): complex_types__day__val(X) <= 65 complex_types__sun may_be_deduced_from 66 [0 <= X, X <= 6]. 67initialize_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]. 70initialize_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]. 73initialize_rules(35): complex_types__day__pos(complex_types__day__val(X)) may_be_replaced_by X 74 if [0 <= X, X <= 6]. 75initialize_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]. 77initialize_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]. 81initialize_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]. 84initialize_rules(39): complex_types__array_index__size >= 0 may_be_deduced. 85initialize_rules(40): complex_types__array_index__first may_be_replaced_by 0. 86initialize_rules(41): complex_types__array_index__last may_be_replaced_by 9. 87initialize_rules(42): complex_types__array_index__base__first may_be_replaced_by -2147483648. 88initialize_rules(43): complex_types__array_index__base__last may_be_replaced_by 2147483647. 89initialize_rules(44): complex_types__record_type__size >= 0 may_be_deduced. 90initialize_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)]. 95