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