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 29-NOV-2010, 14:30:10 SIMPLIFIED 29-NOV-2010, 14:30:11 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 Greatest_Common_Divisor.G_C_D 14 15 16 17 18For path(s) from start to run-time check associated with statement of line 8: 19 20procedure_g_c_d_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_g_c_d_2. 27*** true . /* all conclusions proved */ 28 29 30For path(s) from start to assertion of line 10: 31 32procedure_g_c_d_3. 33*** true . /* all conclusions proved */ 34 35 36For path(s) from assertion of line 10 to assertion of line 10: 37 38procedure_g_c_d_4. 39H1: c >= 0 . 40H2: d > 0 . 41H3: gcd(c, d) = gcd(m, n) . 42H4: m >= 0 . 43H5: m <= 2147483647 . 44H6: n <= 2147483647 . 45H7: n > 0 . 46H8: c <= 2147483647 . 47H9: d <= 2147483647 . 48H10: c - c div d * d >= - 2147483648 . 49H11: c - c div d * d <= 2147483647 . 50H12: c - c div d * d <> 0 . 51H13: integer__size >= 0 . 52H14: natural__size >= 0 . 53 -> 54C1: c - c div d * d > 0 . 55C2: gcd(d, c - c div d * d) = gcd(m, n) . 56 57 58For path(s) from assertion of line 10 to run-time check associated with 59 statement of line 11: 60 61procedure_g_c_d_5. 62*** true . /* all conclusions proved */ 63 64 65For path(s) from assertion of line 10 to run-time check associated with 66 statement of line 12: 67 68procedure_g_c_d_6. 69*** true . /* all conclusions proved */ 70 71 72For path(s) from assertion of line 10 to run-time check associated with 73 statement of line 12: 74 75procedure_g_c_d_7. 76*** true . /* all conclusions proved */ 77 78 79For path(s) from start to run-time check associated with statement of line 14: 80 81procedure_g_c_d_8. 82*** true . /* all conclusions proved */ 83 84 85For path(s) from assertion of line 10 to run-time check associated with 86 statement of line 14: 87 88procedure_g_c_d_9. 89*** true . /* all conclusions proved */ 90 91 92For path(s) from start to finish: 93 94procedure_g_c_d_10. 95*** true . /* contradiction within hypotheses. */ 96 97 98 99For path(s) from assertion of line 10 to finish: 100 101procedure_g_c_d_11. 102H1: c >= 0 . 103H2: d > 0 . 104H3: gcd(c, d) = gcd(m, n) . 105H4: m >= 0 . 106H5: m <= 2147483647 . 107H6: n <= 2147483647 . 108H7: n > 0 . 109H8: c <= 2147483647 . 110H9: d <= 2147483647 . 111H10: c - c div d * d = 0 . 112H11: integer__size >= 0 . 113H12: natural__size >= 0 . 114 -> 115C1: d = gcd(m, n) . 116 117 118