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