File ‹simple_greatest_common_divisor/g_c_d.siv›
*****************************************************************************
Semantic Analysis of SPARK Text
Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
*****************************************************************************
CREATED 22-SEP-2011, 11:10:48 SIMPLIFIED 22-SEP-2011, 11:10:49
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
procedure Simple_Greatest_Common_Divisor.G_C_D
For path(s) from start to run-time check associated with statement of line 8:
procedure_g_c_d_1.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 8:
procedure_g_c_d_2.
*** true . /* all conclusions proved */
For path(s) from start to assertion of line 9:
procedure_g_c_d_3.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to assertion of line 9:
procedure_g_c_d_4.
H1: gcd(c, d) = gcd(m, n) .
H2: m >= 0 .
H3: m <= 2147483647 .
H4: n <= 2147483647 .
H5: n > 0 .
H6: d <= 2147483647 .
H7: c >= 0 .
H8: c <= 2147483647 .
H9: c mod d >= 0 .
H10: c mod d <= 2147483647 .
H11: 0 < d .
H12: integer__size >= 0 .
H13: natural__size >= 0 .
->
C1: gcd(d, c mod d) = gcd(m, n) .
For path(s) from assertion of line 9 to run-time check associated with
statement of line 12:
procedure_g_c_d_5.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to run-time check associated with
statement of line 13:
procedure_g_c_d_6.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to run-time check associated with
statement of line 13:
procedure_g_c_d_7.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to run-time check associated with
statement of line 15:
procedure_g_c_d_8.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to finish:
procedure_g_c_d_9.
H1: gcd(c, 0) = gcd(m, n) .
H2: m >= 0 .
H3: m <= 2147483647 .
H4: n <= 2147483647 .
H5: n > 0 .
H6: c >= 0 .
H7: c <= 2147483647 .
H8: integer__size >= 0 .
H9: natural__size >= 0 .
->
C1: c = gcd(m, n) .