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 22-SEP-2011, 11:10:50  SIMPLIFIED 22-SEP-2011, 11:10:51
9
10SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
11Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
12
13procedure Loop_Invariant.Proc2
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 18:
19
20procedure_proc2_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to run-time check associated with statement of line 19:
25
26procedure_proc2_2.
27*** true .          /* all conclusions proved */
28
29
30For path(s) from start to run-time check associated with statement of line 19:
31
32procedure_proc2_3.
33*** true .          /* all conclusions proved */
34
35
36For path(s) from start to assertion of line 19:
37
38procedure_proc2_4.
39*** true .          /* all conclusions proved */
40
41
42For path(s) from assertion of line 23 to assertion of line 19:
43
44procedure_proc2_5.
45*** true .          /* all conclusions proved */
46
47
48For path(s) from assertion of line 19 to run-time check associated with 
49          statement of line 22:
50
51procedure_proc2_6.
52*** true .          /* all conclusions proved */
53
54
55For path(s) from assertion of line 19 to assertion of line 23:
56
57procedure_proc2_7.
58H1:    a <= 2147483647 .
59H2:    b >= 0 .
60H3:    b <= 4294967295 .
61H4:    loop__1__i <= 2147483647 .
62H5:    loop__1__i >= 1 .
63H6:    loop__1__i <= a .
64H7:    (loop__1__i - 1) * b mod 4294967296 >= 0 .
65H8:    (loop__1__i - 1) * b mod 4294967296 <= 4294967295 .
66H9:    ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 .
67H10:   ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 .
68H11:   integer__size >= 0 .
69H12:   natural__size >= 0 .
70H13:   word32__size >= 0 .
71       ->
72C1:    loop__1__i * b mod 4294967296 = ((loop__1__i - 1) * b mod 4294967296 + b)
73           mod 4294967296 .
74
75
76For path(s) from start to finish:
77
78procedure_proc2_8.
79*** true .          /* all conclusions proved */
80
81
82For path(s) from assertion of line 23 to finish:
83
84procedure_proc2_9.
85*** true .          /* all conclusions proved */
86
87
88