***************************************************************************** Semantic Analysis of SPARK Text Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. ***************************************************************************** CREATED 22-SEP-2011, 11:10:52 SIMPLIFIED 22-SEP-2011, 11:10:53 SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. procedure Complex_Types_App.Initialize For path(s) from start to assertion of line 7: procedure_initialize_1. H1: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H2: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H3: integer__size >= 0 . H4: complex_types__day__size >= 0 . H5: complex_types__array_index__size >= 0 . H6: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized(a, 0) . For path(s) from assertion of line 15 to assertion of line 7: procedure_initialize_2. H1: complex_types__initialized(a, loop__1__i) . H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 9) . H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), 9, complex_types__day__pos(complex_types__sun)) . H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H6: loop__1__i >= 0 . H7: loop__1__i < 9 . H8: integer__size >= 0 . H9: complex_types__day__size >= 0 . H10: complex_types__array_index__size >= 0 . H11: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(upf_field2( element(a, [loop__1__i]), 0), update(fld_field1(element(a, [ loop__1__i])), [9, complex_types__sun], 0))), loop__1__i + 1) . C2: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i], upf_field1(upf_field2(element(a, [loop__1__i]), 0), update(fld_field1( element(a, [loop__1__i])), [9, complex_types__sun], 0))), [i___1])), [ i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i], upf_field1(upf_field2(element(a, [loop__1__i]), 0), update(fld_field1( element(a, [loop__1__i])), [9, complex_types__sun], 0))), [i___1])), [ i___2, i___3]) <= 2147483647))) . For path(s) from assertion of line 7 to assertion of line 10: procedure_initialize_3. H1: complex_types__initialized(a, loop__1__i) . H2: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H3: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H4: loop__1__i >= 0 . H5: loop__1__i <= 9 . H6: integer__size >= 0 . H7: complex_types__day__size >= 0 . H8: complex_types__array_index__size >= 0 . H9: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 0) . For path(s) from assertion of line 15 to assertion of line 10: procedure_initialize_4. H1: complex_types__initialized(a, loop__1__i) . H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), loop__2__j) . H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), loop__2__j, complex_types__day__pos(complex_types__sun)) . H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H6: loop__2__j >= 0 . H7: loop__1__i >= 0 . H8: loop__1__i <= 9 . H9: loop__2__j < 9 . H10: integer__size >= 0 . H11: complex_types__day__size >= 0 . H12: complex_types__array_index__size >= 0 . H13: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [loop__1__i])), [ loop__2__j, complex_types__sun], 0))), loop__1__i) . C2: complex_types__initialized2(update(fld_field1(element(a, [loop__1__i])), [loop__2__j, complex_types__sun], 0), loop__2__j + 1) . C3: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i], upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ loop__1__i])), [loop__2__j, complex_types__sun], 0))), [i___1])), [ i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i], upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ loop__1__i])), [loop__2__j, complex_types__sun], 0))), [i___1])), [ i___2, i___3]) <= 2147483647))) . For path(s) from assertion of line 10 to assertion of line 15: procedure_initialize_5. H1: complex_types__initialized(a, loop__1__i) . H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), loop__2__j) . H3: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H4: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H5: loop__2__j >= 0 . H6: loop__2__j <= 9 . H7: loop__1__i >= 0 . H8: loop__1__i <= 9 . H9: integer__size >= 0 . H10: complex_types__day__size >= 0 . H11: complex_types__array_index__size >= 0 . H12: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), loop__2__j, 0) . For path(s) from assertion of line 15 to assertion of line 15: procedure_initialize_6. H1: complex_types__initialized(a, loop__1__i) . H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), loop__2__j) . H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), loop__2__j, complex_types__day__pos(loop__3__k)) . H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H6: complex_types__mon <= loop__3__k . H7: loop__2__j >= 0 . H8: loop__2__j <= 9 . H9: loop__1__i >= 0 . H10: loop__1__i <= 9 . H11: loop__3__k < complex_types__sun . H12: integer__size >= 0 . H13: complex_types__day__size >= 0 . H14: complex_types__array_index__size >= 0 . H15: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [loop__1__i])), [ loop__2__j, loop__3__k], 0))), loop__1__i) . C2: complex_types__initialized2(update(fld_field1(element(a, [loop__1__i])), [loop__2__j, loop__3__k], 0), loop__2__j) . C3: complex_types__initialized3(update(fld_field1(element(a, [loop__1__i])), [loop__2__j, loop__3__k], 0), loop__2__j, complex_types__day__pos( succ(loop__3__k))) . C4: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i], upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ loop__1__i])), [loop__2__j, loop__3__k], 0))), [i___1])), [i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i], upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [ loop__1__i])), [loop__2__j, loop__3__k], 0))), [i___1])), [i___2, i___3]) <= 2147483647))) . For path(s) from assertion of line 15 to run-time check associated with statement of line 22: procedure_initialize_7. *** true . /* all conclusions proved */ For path(s) from assertion of line 15 to run-time check associated with statement of line 25: procedure_initialize_8. *** true . /* all conclusions proved */ For path(s) from assertion of line 15 to finish: procedure_initialize_9. H1: complex_types__initialized(a, 9) . H2: complex_types__initialized2(fld_field1(element(a, [9])), 9) . H3: complex_types__initialized3(fld_field1(element(a, [9])), 9, complex_types__day__pos(complex_types__sun)) . H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1])) <= 2147483647) . H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2 and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2, i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3]) <= 2147483647))) . H6: integer__size >= 0 . H7: complex_types__day__size >= 0 . H8: complex_types__array_index__size >= 0 . H9: complex_types__record_type__size >= 0 . -> C1: complex_types__initialized(update(a, [9], upf_field1(upf_field2(element( a, [9]), 0), update(fld_field1(element(a, [9])), [9, complex_types__sun], 0))), 10) .