src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.siv
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.siv	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,118 @@
     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:19  SIMPLIFIED 29-NOV-2010, 14:30:21
    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 +function RMD.K_R
    1.17 +
    1.18 +
    1.19 +
    1.20 +
    1.21 +For path(s) from start to run-time check associated with statement of line 38:
    1.22 +
    1.23 +function_k_r_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 39:
    1.28 +
    1.29 +function_k_r_2.
    1.30 +*** true .          /* all conclusions proved */
    1.31 +
    1.32 +
    1.33 +For path(s) from start to run-time check associated with statement of line 40:
    1.34 +
    1.35 +function_k_r_3.
    1.36 +*** true .          /* all conclusions proved */
    1.37 +
    1.38 +
    1.39 +For path(s) from start to run-time check associated with statement of line 41:
    1.40 +
    1.41 +function_k_r_4.
    1.42 +*** true .          /* all conclusions proved */
    1.43 +
    1.44 +
    1.45 +For path(s) from start to run-time check associated with statement of line 42:
    1.46 +
    1.47 +function_k_r_5.
    1.48 +*** true .          /* all conclusions proved */
    1.49 +
    1.50 +
    1.51 +For path(s) from start to finish:
    1.52 +
    1.53 +function_k_r_6.
    1.54 +H1:    j >= 0 .
    1.55 +H2:    j <= 15 .
    1.56 +H3:    interfaces__unsigned_32__size >= 0 .
    1.57 +H4:    word__size >= 0 .
    1.58 +H5:    round_index__size >= 0 .
    1.59 +H6:    round_index__base__first <= round_index__base__last .
    1.60 +H7:    round_index__base__first <= 0 .
    1.61 +H8:    round_index__base__last >= 79 .
    1.62 +       ->
    1.63 +C1:    1352829926 = k_r_spec(j) .
    1.64 +
    1.65 +
    1.66 +function_k_r_7.
    1.67 +H1:    16 <= j .
    1.68 +H2:    j <= 31 .
    1.69 +H3:    interfaces__unsigned_32__size >= 0 .
    1.70 +H4:    word__size >= 0 .
    1.71 +H5:    round_index__size >= 0 .
    1.72 +H6:    round_index__base__first <= round_index__base__last .
    1.73 +H7:    round_index__base__first <= 0 .
    1.74 +H8:    round_index__base__last >= 79 .
    1.75 +       ->
    1.76 +C1:    1548603684 = k_r_spec(j) .
    1.77 +
    1.78 +
    1.79 +function_k_r_8.
    1.80 +H1:    32 <= j .
    1.81 +H2:    j <= 47 .
    1.82 +H3:    interfaces__unsigned_32__size >= 0 .
    1.83 +H4:    word__size >= 0 .
    1.84 +H5:    round_index__size >= 0 .
    1.85 +H6:    round_index__base__first <= round_index__base__last .
    1.86 +H7:    round_index__base__first <= 0 .
    1.87 +H8:    round_index__base__last >= 79 .
    1.88 +       ->
    1.89 +C1:    1836072691 = k_r_spec(j) .
    1.90 +
    1.91 +
    1.92 +function_k_r_9.
    1.93 +H1:    48 <= j .
    1.94 +H2:    j <= 63 .
    1.95 +H3:    interfaces__unsigned_32__size >= 0 .
    1.96 +H4:    word__size >= 0 .
    1.97 +H5:    round_index__size >= 0 .
    1.98 +H6:    round_index__base__first <= round_index__base__last .
    1.99 +H7:    round_index__base__first <= 0 .
   1.100 +H8:    round_index__base__last >= 79 .
   1.101 +       ->
   1.102 +C1:    2053994217 = k_r_spec(j) .
   1.103 +
   1.104 +
   1.105 +function_k_r_10.
   1.106 +H1:    j >= 0 .
   1.107 +H2:    j <= 79 .
   1.108 +H3:    15 < j .
   1.109 +H4:    31 < j .
   1.110 +H5:    47 < j .
   1.111 +H6:    63 < j .
   1.112 +H7:    interfaces__unsigned_32__size >= 0 .
   1.113 +H8:    word__size >= 0 .
   1.114 +H9:    round_index__size >= 0 .
   1.115 +H10:   round_index__base__first <= round_index__base__last .
   1.116 +H11:   round_index__base__first <= 0 .
   1.117 +H12:   round_index__base__last >= 79 .
   1.118 +       ->
   1.119 +C1:    0 = k_r_spec(j) .
   1.120 +
   1.121 +