src/HOL/SPARK/Examples/Sqrt/sqrt/isqrt.siv
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 41561 d1318f3c86ba
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
*****************************************************************************
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     2
                       Semantic Analysis of SPARK Text
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     3
    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     4
             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     5
*****************************************************************************
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     6
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     7
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     8
CREATED 29-NOV-2010, 14:30:17  SIMPLIFIED 29-NOV-2010, 14:30:18
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     9
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    10
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    11
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    12
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    13
function Sqrt.Isqrt
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    14
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    15
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    16
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    17
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    18
For path(s) from start to run-time check associated with statement of line 7:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    19
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    20
function_isqrt_1.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    21
*** true .          /* all conclusions proved */
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    22
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    23
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    24
For path(s) from start to assertion of line 9:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    25
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    26
function_isqrt_2.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    27
*** true .          /* all conclusions proved */
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    28
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    29
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    30
For path(s) from assertion of line 9 to assertion of line 9:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    31
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    32
function_isqrt_3.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    33
*** true .          /* all conclusions proved */
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    34
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    35
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    36
For path(s) from assertion of line 9 to run-time check associated with 
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    37
          statement of line 10:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    38
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    39
function_isqrt_4.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    40
H1:    r * r <= n .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    41
H2:    n >= 0 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    42
H3:    n <= 2147483647 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    43
H4:    r >= 0 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    44
H5:    r <= 2147483647 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    45
H6:    integer__size >= 0 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    46
H7:    natural__size >= 0 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    47
       ->
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    48
C1:    2 * r <= 2147483646 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    49
C2:    2 * r <= 2147483647 .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    50
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    51
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    52
For path(s) from assertion of line 9 to run-time check associated with 
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    53
          statement of line 11:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    54
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    55
function_isqrt_5.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    56
*** true .          /* all conclusions proved */
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    57
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    58
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    59
For path(s) from assertion of line 9 to finish:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    60
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    61
function_isqrt_6.
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    62
*** true .          /* all conclusions proved */
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    63
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    64