41561
|
1 |
*****************************************************************************
|
|
2 |
Semantic Analysis of SPARK Text
|
|
3 |
Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
|
|
4 |
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
|
|
5 |
*****************************************************************************
|
|
6 |
|
|
7 |
|
|
8 |
CREATED 29-NOV-2010, 14:30:17 SIMPLIFIED 29-NOV-2010, 14:30:18
|
|
9 |
|
|
10 |
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
|
|
11 |
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
|
|
12 |
|
|
13 |
function Sqrt.Isqrt
|
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
|
|
18 |
For path(s) from start to run-time check associated with statement of line 7:
|
|
19 |
|
|
20 |
function_isqrt_1.
|
|
21 |
*** true . /* all conclusions proved */
|
|
22 |
|
|
23 |
|
|
24 |
For path(s) from start to assertion of line 9:
|
|
25 |
|
|
26 |
function_isqrt_2.
|
|
27 |
*** true . /* all conclusions proved */
|
|
28 |
|
|
29 |
|
|
30 |
For path(s) from assertion of line 9 to assertion of line 9:
|
|
31 |
|
|
32 |
function_isqrt_3.
|
|
33 |
*** true . /* all conclusions proved */
|
|
34 |
|
|
35 |
|
|
36 |
For path(s) from assertion of line 9 to run-time check associated with
|
|
37 |
statement of line 10:
|
|
38 |
|
|
39 |
function_isqrt_4.
|
|
40 |
H1: r * r <= n .
|
|
41 |
H2: n >= 0 .
|
|
42 |
H3: n <= 2147483647 .
|
|
43 |
H4: r >= 0 .
|
|
44 |
H5: r <= 2147483647 .
|
|
45 |
H6: integer__size >= 0 .
|
|
46 |
H7: natural__size >= 0 .
|
|
47 |
->
|
|
48 |
C1: 2 * r <= 2147483646 .
|
|
49 |
C2: 2 * r <= 2147483647 .
|
|
50 |
|
|
51 |
|
|
52 |
For path(s) from assertion of line 9 to run-time check associated with
|
|
53 |
statement of line 11:
|
|
54 |
|
|
55 |
function_isqrt_5.
|
|
56 |
*** true . /* all conclusions proved */
|
|
57 |
|
|
58 |
|
|
59 |
For path(s) from assertion of line 9 to finish:
|
|
60 |
|
|
61 |
function_isqrt_6.
|
|
62 |
*** true . /* all conclusions proved */
|
|
63 |
|
|
64 |
|