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.Proc1
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 7:
19
20procedure_proc1_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to run-time check associated with statement of line 8:
25
26procedure_proc1_2.
27*** true .          /* all conclusions proved */
28
29
30For path(s) from start to run-time check associated with statement of line 8:
31
32procedure_proc1_3.
33*** true .          /* all conclusions proved */
34
35
36For path(s) from start to assertion of line 8:
37
38procedure_proc1_4.
39*** true .          /* all conclusions proved */
40
41
42For path(s) from assertion of line 8 to assertion of line 8:
43
44procedure_proc1_5.
45H1:    a <= 2147483647 .
46H2:    b >= 0 .
47H3:    b <= 4294967295 .
48H4:    loop__1__i >= 1 .
49H5:    (loop__1__i - 1) * b mod 4294967296 >= 0 .
50H6:    (loop__1__i - 1) * b mod 4294967296 <= 4294967295 .
51H7:    ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 .
52H8:    ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 .
53H9:    loop__1__i < a .
54H10:   integer__size >= 0 .
55H11:   natural__size >= 0 .
56H12:   word32__size >= 0 .
57       ->
58C1:    loop__1__i * b mod 4294967296 = ((loop__1__i - 1) * b mod 4294967296 + b)
59           mod 4294967296 .
60
61
62For path(s) from assertion of line 8 to run-time check associated with 
63          statement of line 11:
64
65procedure_proc1_6.
66*** true .          /* all conclusions proved */
67
68
69For path(s) from start to finish:
70
71procedure_proc1_7.
72*** true .          /* all conclusions proved */
73
74
75For path(s) from assertion of line 8 to finish:
76
77procedure_proc1_8.
78H1:    a <= 2147483647 .
79H2:    b >= 0 .
80H3:    b <= 4294967295 .
81H4:    a <= 2147483647 .
82H5:    a >= 1 .
83H6:    (a - 1) * b mod 4294967296 >= 0 .
84H7:    (a - 1) * b mod 4294967296 <= 4294967295 .
85H8:    ((a - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 .
86H9:    ((a - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 .
87H10:   integer__size >= 0 .
88H11:   natural__size >= 0 .
89H12:   word32__size >= 0 .
90       ->
91C1:    a * b mod 4294967296 = ((a - 1) * b mod 4294967296 + b) mod 4294967296 .
92
93
94