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