1***************************************************************************** 2 Semantic Analysis of SPARK Text 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 8CREATED 22-SEP-2011, 11:10:52 SIMPLIFIED 22-SEP-2011, 11:10:53 9 10SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 11Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. 12 13procedure Complex_Types_App.Initialize 14 15 16 17 18For path(s) from start to assertion of line 7: 19 20procedure_initialize_1. 21H1: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 22 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 23 <= 2147483647) . 24H2: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 25 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 26 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 27 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 28 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 29 <= 2147483647))) . 30H3: integer__size >= 0 . 31H4: complex_types__day__size >= 0 . 32H5: complex_types__array_index__size >= 0 . 33H6: complex_types__record_type__size >= 0 . 34 -> 35C1: complex_types__initialized(a, 0) . 36 37 38For path(s) from assertion of line 15 to assertion of line 7: 39 40procedure_initialize_2. 41H1: complex_types__initialized(a, loop__1__i) . 42H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 9) . 43H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), 9, 44 complex_types__day__pos(complex_types__sun)) . 45H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 46 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 47 <= 2147483647) . 48H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 49 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 50 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 51 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 52 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 53 <= 2147483647))) . 54H6: loop__1__i >= 0 . 55H7: loop__1__i < 9 . 56H8: integer__size >= 0 . 57H9: complex_types__day__size >= 0 . 58H10: complex_types__array_index__size >= 0 . 59H11: complex_types__record_type__size >= 0 . 60 -> 61C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(upf_field2( 62 element(a, [loop__1__i]), 0), update(fld_field1(element(a, [ 63 loop__1__i])), [9, complex_types__sun], 0))), loop__1__i + 1) . 64C2: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 65 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 66 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 67 -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i], 68 upf_field1(upf_field2(element(a, [loop__1__i]), 0), update(fld_field1( 69 element(a, [loop__1__i])), [9, complex_types__sun], 0))), [i___1])), [ 70 i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i], 71 upf_field1(upf_field2(element(a, [loop__1__i]), 0), update(fld_field1( 72 element(a, [loop__1__i])), [9, complex_types__sun], 0))), [i___1])), [ 73 i___2, i___3]) <= 2147483647))) . 74 75 76For path(s) from assertion of line 7 to assertion of line 10: 77 78procedure_initialize_3. 79H1: complex_types__initialized(a, loop__1__i) . 80H2: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 81 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 82 <= 2147483647) . 83H3: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 84 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 85 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 86 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 87 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 88 <= 2147483647))) . 89H4: loop__1__i >= 0 . 90H5: loop__1__i <= 9 . 91H6: integer__size >= 0 . 92H7: complex_types__day__size >= 0 . 93H8: complex_types__array_index__size >= 0 . 94H9: complex_types__record_type__size >= 0 . 95 -> 96C1: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 0) . 97 98 99For path(s) from assertion of line 15 to assertion of line 10: 100 101procedure_initialize_4. 102H1: complex_types__initialized(a, loop__1__i) . 103H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 104 loop__2__j) . 105H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), 106 loop__2__j, complex_types__day__pos(complex_types__sun)) . 107H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 108 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 109 <= 2147483647) . 110H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 111 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 112 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 113 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 114 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 115 <= 2147483647))) . 116H6: loop__2__j >= 0 . 117H7: loop__1__i >= 0 . 118H8: loop__1__i <= 9 . 119H9: loop__2__j < 9 . 120H10: integer__size >= 0 . 121H11: complex_types__day__size >= 0 . 122H12: complex_types__array_index__size >= 0 . 123H13: complex_types__record_type__size >= 0 . 124 -> 125C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(element(a, 126 [loop__1__i]), update(fld_field1(element(a, [loop__1__i])), [ 127 loop__2__j, complex_types__sun], 0))), loop__1__i) . 128C2: complex_types__initialized2(update(fld_field1(element(a, [loop__1__i])), 129 [loop__2__j, complex_types__sun], 0), loop__2__j + 1) . 130C3: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 131 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 132 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 133 -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i], 134 upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ 135 loop__1__i])), [loop__2__j, complex_types__sun], 0))), [i___1])), [ 136 i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i], 137 upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ 138 loop__1__i])), [loop__2__j, complex_types__sun], 0))), [i___1])), [ 139 i___2, i___3]) <= 2147483647))) . 140 141 142For path(s) from assertion of line 10 to assertion of line 15: 143 144procedure_initialize_5. 145H1: complex_types__initialized(a, loop__1__i) . 146H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 147 loop__2__j) . 148H3: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 149 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 150 <= 2147483647) . 151H4: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 152 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 153 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 154 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 155 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 156 <= 2147483647))) . 157H5: loop__2__j >= 0 . 158H6: loop__2__j <= 9 . 159H7: loop__1__i >= 0 . 160H8: loop__1__i <= 9 . 161H9: integer__size >= 0 . 162H10: complex_types__day__size >= 0 . 163H11: complex_types__array_index__size >= 0 . 164H12: complex_types__record_type__size >= 0 . 165 -> 166C1: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), 167 loop__2__j, 0) . 168 169 170For path(s) from assertion of line 15 to assertion of line 15: 171 172procedure_initialize_6. 173H1: complex_types__initialized(a, loop__1__i) . 174H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 175 loop__2__j) . 176H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), 177 loop__2__j, complex_types__day__pos(loop__3__k)) . 178H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 179 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 180 <= 2147483647) . 181H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 182 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 183 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 184 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 185 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 186 <= 2147483647))) . 187H6: complex_types__mon <= loop__3__k . 188H7: loop__2__j >= 0 . 189H8: loop__2__j <= 9 . 190H9: loop__1__i >= 0 . 191H10: loop__1__i <= 9 . 192H11: loop__3__k < complex_types__sun . 193H12: integer__size >= 0 . 194H13: complex_types__day__size >= 0 . 195H14: complex_types__array_index__size >= 0 . 196H15: complex_types__record_type__size >= 0 . 197 -> 198C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(element(a, 199 [loop__1__i]), update(fld_field1(element(a, [loop__1__i])), [ 200 loop__2__j, loop__3__k], 0))), loop__1__i) . 201C2: complex_types__initialized2(update(fld_field1(element(a, [loop__1__i])), 202 [loop__2__j, loop__3__k], 0), loop__2__j) . 203C3: complex_types__initialized3(update(fld_field1(element(a, [loop__1__i])), 204 [loop__2__j, loop__3__k], 0), loop__2__j, complex_types__day__pos( 205 succ(loop__3__k))) . 206C4: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 207 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 208 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 209 -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i], 210 upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ 211 loop__1__i])), [loop__2__j, loop__3__k], 0))), [i___1])), [i___2, 212 i___3]) and element(fld_field1(element(update(a, [loop__1__i], 213 upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ 214 loop__1__i])), [loop__2__j, loop__3__k], 0))), [i___1])), [i___2, 215 i___3]) <= 2147483647))) . 216 217 218For path(s) from assertion of line 15 to run-time check associated with 219 statement of line 22: 220 221procedure_initialize_7. 222*** true . /* all conclusions proved */ 223 224 225For path(s) from assertion of line 15 to run-time check associated with 226 statement of line 25: 227 228procedure_initialize_8. 229*** true . /* all conclusions proved */ 230 231 232For path(s) from assertion of line 15 to finish: 233 234procedure_initialize_9. 235H1: complex_types__initialized(a, 9) . 236H2: complex_types__initialized2(fld_field1(element(a, [9])), 9) . 237H3: complex_types__initialized3(fld_field1(element(a, [9])), 9, 238 complex_types__day__pos(complex_types__sun)) . 239H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= 240 fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) 241 <= 2147483647) . 242H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and 243 i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 244 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 245 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, 246 i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) 247 <= 2147483647))) . 248H6: integer__size >= 0 . 249H7: complex_types__day__size >= 0 . 250H8: complex_types__array_index__size >= 0 . 251H9: complex_types__record_type__size >= 0 . 252 -> 253C1: complex_types__initialized(update(a, [9], upf_field1(upf_field2(element( 254 a, [9]), 0), update(fld_field1(element(a, [9])), [9, 255 complex_types__sun], 0))), 10) . 256 257 258