src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls
author berghofe
Sat Jan 15 12:35:29 2011 +0100 (2011-01-15)
changeset 41561 d1318f3c86ba
permissions -rw-r--r--
Added new SPARK verification environment.
berghofe@41561
     1
           /*********************************************************/
berghofe@41561
     2
                           /*Proof Rule Declarations*/
berghofe@41561
     3
    /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
berghofe@41561
     4
             /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
berghofe@41561
     5
           /*********************************************************/
berghofe@41561
     6
berghofe@41561
     7
berghofe@41561
     8
                        /*DATE : 29-NOV-2010 14:30:10.98*/
berghofe@41561
     9
berghofe@41561
    10
                  /*procedure Greatest_Common_Divisor.G_C_D*/
berghofe@41561
    11
berghofe@41561
    12
berghofe@41561
    13
rule_family g_c_d_rules:
berghofe@41561
    14
     X      requires [X:any] &
berghofe@41561
    15
     X <= Y requires [X:ire, Y:ire] &
berghofe@41561
    16
     X >= Y requires [X:ire, Y:ire].
berghofe@41561
    17
berghofe@41561
    18
g_c_d_rules(1): integer__size >= 0 may_be_deduced.
berghofe@41561
    19
g_c_d_rules(2): integer__first may_be_replaced_by -2147483648.
berghofe@41561
    20
g_c_d_rules(3): integer__last may_be_replaced_by 2147483647.
berghofe@41561
    21
g_c_d_rules(4): integer__base__first may_be_replaced_by -2147483648.
berghofe@41561
    22
g_c_d_rules(5): integer__base__last may_be_replaced_by 2147483647.
berghofe@41561
    23
g_c_d_rules(6): natural__size >= 0 may_be_deduced.
berghofe@41561
    24
g_c_d_rules(7): natural__first may_be_replaced_by 0.
berghofe@41561
    25
g_c_d_rules(8): natural__last may_be_replaced_by 2147483647.
berghofe@41561
    26
g_c_d_rules(9): natural__base__first may_be_replaced_by -2147483648.
berghofe@41561
    27
g_c_d_rules(10): natural__base__last may_be_replaced_by 2147483647.