|
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:19 SIMPLIFIED 29-NOV-2010, 14:30:21
|
|
|
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 RMD.R_R
|
|
|
14 |
|
|
|
15 |
|
|
|
16 |
|
|
|
17 |
|
|
|
18 |
For path(s) from start to run-time check associated with statement of line 73:
|
|
|
19 |
|
|
|
20 |
function_r_r_1.
|
|
|
21 |
*** true . /* all conclusions proved */
|
|
|
22 |
|
|
|
23 |
|
|
|
24 |
For path(s) from start to finish:
|
|
|
25 |
|
|
|
26 |
function_r_r_2.
|
|
|
27 |
H1: j >= 0 .
|
|
|
28 |
H2: j <= 79 .
|
|
|
29 |
H3: block_index__size >= 0 .
|
|
|
30 |
H4: block_index__base__first <= block_index__base__last .
|
|
|
31 |
H5: round_index__size >= 0 .
|
|
|
32 |
H6: round_index__base__first <= round_index__base__last .
|
|
|
33 |
H7: block_index__base__first <= 0 .
|
|
|
34 |
H8: block_index__base__last >= 15 .
|
|
|
35 |
H9: round_index__base__first <= 0 .
|
|
|
36 |
H10: round_index__base__last >= 79 .
|
|
|
37 |
->
|
|
|
38 |
C1: element(mk__block_permutation([0] := 5, [1] := 14, [2] := 7, [3] := 0, [
|
|
|
39 |
4] := 9, [5] := 2, [6] := 11, [7] := 4, [8] := 13, [9] := 6, [10] :=
|
|
|
40 |
15, [11] := 8, [12] := 1, [13] := 10, [14] := 3, [15] := 12, [16] :=
|
|
|
41 |
6, [17] := 11, [18] := 3, [19] := 7, [20] := 0, [21] := 13, [22] :=
|
|
|
42 |
5, [23] := 10, [24] := 14, [25] := 15, [26] := 8, [27] := 12, [28] :=
|
|
|
43 |
4, [29] := 9, [30] := 1, [31] := 2, [32] := 15, [33] := 5, [34] := 1,
|
|
|
44 |
[35] := 3, [36] := 7, [37] := 14, [38] := 6, [39] := 9, [40] := 11, [
|
|
|
45 |
41] := 8, [42] := 12, [43] := 2, [44] := 10, [45] := 0, [46] := 4, [
|
|
|
46 |
47] := 13, [48] := 8, [49] := 6, [50] := 4, [51] := 1, [52] := 3, [53]
|
|
|
47 |
:= 11, [54] := 15, [55] := 0, [56] := 5, [57] := 12, [58] := 2, [59]
|
|
|
48 |
:= 13, [60] := 9, [61] := 7, [62] := 10, [63] := 14, [64] := 12, [65]
|
|
|
49 |
:= 15, [66] := 10, [67] := 4, [68] := 1, [69] := 5, [70] := 8, [71]
|
|
|
50 |
:= 7, [72] := 6, [73] := 2, [74] := 13, [75] := 14, [76] := 0, [77]
|
|
|
51 |
:= 3, [78] := 9, [79] := 11), [j]) = r_r_spec(j) .
|
|
|
52 |
C2: element(mk__block_permutation([0] := 5, [1] := 14, [2] := 7, [3] := 0, [
|
|
|
53 |
4] := 9, [5] := 2, [6] := 11, [7] := 4, [8] := 13, [9] := 6, [10] :=
|
|
|
54 |
15, [11] := 8, [12] := 1, [13] := 10, [14] := 3, [15] := 12, [16] :=
|
|
|
55 |
6, [17] := 11, [18] := 3, [19] := 7, [20] := 0, [21] := 13, [22] :=
|
|
|
56 |
5, [23] := 10, [24] := 14, [25] := 15, [26] := 8, [27] := 12, [28] :=
|
|
|
57 |
4, [29] := 9, [30] := 1, [31] := 2, [32] := 15, [33] := 5, [34] := 1,
|
|
|
58 |
[35] := 3, [36] := 7, [37] := 14, [38] := 6, [39] := 9, [40] := 11, [
|
|
|
59 |
41] := 8, [42] := 12, [43] := 2, [44] := 10, [45] := 0, [46] := 4, [
|
|
|
60 |
47] := 13, [48] := 8, [49] := 6, [50] := 4, [51] := 1, [52] := 3, [53]
|
|
|
61 |
:= 11, [54] := 15, [55] := 0, [56] := 5, [57] := 12, [58] := 2, [59]
|
|
|
62 |
:= 13, [60] := 9, [61] := 7, [62] := 10, [63] := 14, [64] := 12, [65]
|
|
|
63 |
:= 15, [66] := 10, [67] := 4, [68] := 1, [69] := 5, [70] := 8, [71]
|
|
|
64 |
:= 7, [72] := 6, [73] := 2, [74] := 13, [75] := 14, [76] := 0, [77]
|
|
|
65 |
:= 3, [78] := 9, [79] := 11), [j]) >= 0 .
|
|
|
66 |
C3: element(mk__block_permutation([0] := 5, [1] := 14, [2] := 7, [3] := 0, [
|
|
|
67 |
4] := 9, [5] := 2, [6] := 11, [7] := 4, [8] := 13, [9] := 6, [10] :=
|
|
|
68 |
15, [11] := 8, [12] := 1, [13] := 10, [14] := 3, [15] := 12, [16] :=
|
|
|
69 |
6, [17] := 11, [18] := 3, [19] := 7, [20] := 0, [21] := 13, [22] :=
|
|
|
70 |
5, [23] := 10, [24] := 14, [25] := 15, [26] := 8, [27] := 12, [28] :=
|
|
|
71 |
4, [29] := 9, [30] := 1, [31] := 2, [32] := 15, [33] := 5, [34] := 1,
|
|
|
72 |
[35] := 3, [36] := 7, [37] := 14, [38] := 6, [39] := 9, [40] := 11, [
|
|
|
73 |
41] := 8, [42] := 12, [43] := 2, [44] := 10, [45] := 0, [46] := 4, [
|
|
|
74 |
47] := 13, [48] := 8, [49] := 6, [50] := 4, [51] := 1, [52] := 3, [53]
|
|
|
75 |
:= 11, [54] := 15, [55] := 0, [56] := 5, [57] := 12, [58] := 2, [59]
|
|
|
76 |
:= 13, [60] := 9, [61] := 7, [62] := 10, [63] := 14, [64] := 12, [65]
|
|
|
77 |
:= 15, [66] := 10, [67] := 4, [68] := 1, [69] := 5, [70] := 8, [71]
|
|
|
78 |
:= 7, [72] := 6, [73] := 2, [74] := 13, [75] := 14, [76] := 0, [77]
|
|
|
79 |
:= 3, [78] := 9, [79] := 11), [j]) <= 15 .
|
|
|
80 |
|
|
|
81 |
|