src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,117 @@
     1.4 +*****************************************************************************
     1.5 +                       Semantic Analysis of SPARK Text
     1.6 +    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
     1.7 +             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
     1.8 +*****************************************************************************
     1.9 +
    1.10 +
    1.11 +CREATED 29-NOV-2010, 14:30:10  SIMPLIFIED 29-NOV-2010, 14:30:11
    1.12 +
    1.13 +SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
    1.14 +Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
    1.15 +
    1.16 +procedure Greatest_Common_Divisor.G_C_D
    1.17 +
    1.18 +
    1.19 +
    1.20 +
    1.21 +For path(s) from start to run-time check associated with statement of line 8:
    1.22 +
    1.23 +procedure_g_c_d_1.
    1.24 +*** true .          /* all conclusions proved */
    1.25 +
    1.26 +
    1.27 +For path(s) from start to run-time check associated with statement of line 8:
    1.28 +
    1.29 +procedure_g_c_d_2.
    1.30 +*** true .          /* all conclusions proved */
    1.31 +
    1.32 +
    1.33 +For path(s) from start to assertion of line 10:
    1.34 +
    1.35 +procedure_g_c_d_3.
    1.36 +*** true .          /* all conclusions proved */
    1.37 +
    1.38 +
    1.39 +For path(s) from assertion of line 10 to assertion of line 10:
    1.40 +
    1.41 +procedure_g_c_d_4.
    1.42 +H1:    c >= 0 .
    1.43 +H2:    d > 0 .
    1.44 +H3:    gcd(c, d) = gcd(m, n) .
    1.45 +H4:    m >= 0 .
    1.46 +H5:    m <= 2147483647 .
    1.47 +H6:    n <= 2147483647 .
    1.48 +H7:    n > 0 .
    1.49 +H8:    c <= 2147483647 .
    1.50 +H9:    d <= 2147483647 .
    1.51 +H10:   c - c div d * d >= - 2147483648 .
    1.52 +H11:   c - c div d * d <= 2147483647 .
    1.53 +H12:   c - c div d * d <> 0 .
    1.54 +H13:   integer__size >= 0 .
    1.55 +H14:   natural__size >= 0 .
    1.56 +       ->
    1.57 +C1:    c - c div d * d > 0 .
    1.58 +C2:    gcd(d, c - c div d * d) = gcd(m, n) .
    1.59 +
    1.60 +
    1.61 +For path(s) from assertion of line 10 to run-time check associated with 
    1.62 +          statement of line 11:
    1.63 +
    1.64 +procedure_g_c_d_5.
    1.65 +*** true .          /* all conclusions proved */
    1.66 +
    1.67 +
    1.68 +For path(s) from assertion of line 10 to run-time check associated with 
    1.69 +          statement of line 12:
    1.70 +
    1.71 +procedure_g_c_d_6.
    1.72 +*** true .          /* all conclusions proved */
    1.73 +
    1.74 +
    1.75 +For path(s) from assertion of line 10 to run-time check associated with 
    1.76 +          statement of line 12:
    1.77 +
    1.78 +procedure_g_c_d_7.
    1.79 +*** true .          /* all conclusions proved */
    1.80 +
    1.81 +
    1.82 +For path(s) from start to run-time check associated with statement of line 14:
    1.83 +
    1.84 +procedure_g_c_d_8.
    1.85 +*** true .          /* all conclusions proved */
    1.86 +
    1.87 +
    1.88 +For path(s) from assertion of line 10 to run-time check associated with 
    1.89 +          statement of line 14:
    1.90 +
    1.91 +procedure_g_c_d_9.
    1.92 +*** true .          /* all conclusions proved */
    1.93 +
    1.94 +
    1.95 +For path(s) from start to finish:
    1.96 +
    1.97 +procedure_g_c_d_10.
    1.98 +*** true .   /* contradiction within hypotheses. */
    1.99 +
   1.100 +
   1.101 +
   1.102 +For path(s) from assertion of line 10 to finish:
   1.103 +
   1.104 +procedure_g_c_d_11.
   1.105 +H1:    c >= 0 .
   1.106 +H2:    d > 0 .
   1.107 +H3:    gcd(c, d) = gcd(m, n) .
   1.108 +H4:    m >= 0 .
   1.109 +H5:    m <= 2147483647 .
   1.110 +H6:    n <= 2147483647 .
   1.111 +H7:    n > 0 .
   1.112 +H8:    c <= 2147483647 .
   1.113 +H9:    d <= 2147483647 .
   1.114 +H10:   c - c div d * d = 0 .
   1.115 +H11:   integer__size >= 0 .
   1.116 +H12:   natural__size >= 0 .
   1.117 +       ->
   1.118 +C1:    d = gcd(m, n) .
   1.119 +
   1.120 +