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:48 SIMPLIFIED 22-SEP-2011, 11:10:49 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 Simple_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 9: 31 32procedure_g_c_d_3. 33*** true . /* all conclusions proved */ 34 35 36For path(s) from assertion of line 9 to assertion of line 9: 37 38procedure_g_c_d_4. 39H1: gcd(c, d) = gcd(m, n) . 40H2: m >= 0 . 41H3: m <= 2147483647 . 42H4: n <= 2147483647 . 43H5: n > 0 . 44H6: d <= 2147483647 . 45H7: c >= 0 . 46H8: c <= 2147483647 . 47H9: c mod d >= 0 . 48H10: c mod d <= 2147483647 . 49H11: 0 < d . 50H12: integer__size >= 0 . 51H13: natural__size >= 0 . 52 -> 53C1: gcd(d, c mod d) = gcd(m, n) . 54 55 56For path(s) from assertion of line 9 to run-time check associated with 57 statement of line 12: 58 59procedure_g_c_d_5. 60*** true . /* all conclusions proved */ 61 62 63For path(s) from assertion of line 9 to run-time check associated with 64 statement of line 13: 65 66procedure_g_c_d_6. 67*** true . /* all conclusions proved */ 68 69 70For path(s) from assertion of line 9 to run-time check associated with 71 statement of line 13: 72 73procedure_g_c_d_7. 74*** true . /* all conclusions proved */ 75 76 77For path(s) from assertion of line 9 to run-time check associated with 78 statement of line 15: 79 80procedure_g_c_d_8. 81*** true . /* all conclusions proved */ 82 83 84For path(s) from assertion of line 9 to finish: 85 86procedure_g_c_d_9. 87H1: gcd(c, 0) = gcd(m, n) . 88H2: m >= 0 . 89H3: m <= 2147483647 . 90H4: n <= 2147483647 . 91H5: n > 0 . 92H6: c >= 0 . 93H7: c <= 2147483647 . 94H8: integer__size >= 0 . 95H9: natural__size >= 0 . 96 -> 97C1: c = gcd(m, n) . 98 99 100