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:50 SIMPLIFIED 22-SEP-2011, 11:10:51 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 Loop_Invariant.Proc2 14 15 16 17 18For path(s) from start to run-time check associated with statement of line 18: 19 20procedure_proc2_1. 21*** true . /* all conclusions proved */ 22 23 24For path(s) from start to run-time check associated with statement of line 19: 25 26procedure_proc2_2. 27*** true . /* all conclusions proved */ 28 29 30For path(s) from start to run-time check associated with statement of line 19: 31 32procedure_proc2_3. 33*** true . /* all conclusions proved */ 34 35 36For path(s) from start to assertion of line 19: 37 38procedure_proc2_4. 39*** true . /* all conclusions proved */ 40 41 42For path(s) from assertion of line 23 to assertion of line 19: 43 44procedure_proc2_5. 45*** true . /* all conclusions proved */ 46 47 48For path(s) from assertion of line 19 to run-time check associated with 49 statement of line 22: 50 51procedure_proc2_6. 52*** true . /* all conclusions proved */ 53 54 55For path(s) from assertion of line 19 to assertion of line 23: 56 57procedure_proc2_7. 58H1: a <= 2147483647 . 59H2: b >= 0 . 60H3: b <= 4294967295 . 61H4: loop__1__i <= 2147483647 . 62H5: loop__1__i >= 1 . 63H6: loop__1__i <= a . 64H7: (loop__1__i - 1) * b mod 4294967296 >= 0 . 65H8: (loop__1__i - 1) * b mod 4294967296 <= 4294967295 . 66H9: ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 . 67H10: ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 . 68H11: integer__size >= 0 . 69H12: natural__size >= 0 . 70H13: word32__size >= 0 . 71 -> 72C1: loop__1__i * b mod 4294967296 = ((loop__1__i - 1) * b mod 4294967296 + b) 73 mod 4294967296 . 74 75 76For path(s) from start to finish: 77 78procedure_proc2_8. 79*** true . /* all conclusions proved */ 80 81 82For path(s) from assertion of line 23 to finish: 83 84procedure_proc2_9. 85*** true . /* all conclusions proved */ 86 87 88