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