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:19 SIMPLIFIED 29-NOV-2010, 14:30:21 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 RMD.R_R 14 15 16 17 18For path(s) from start to run-time check associated with statement of line 73: 19 20function_r_r_1. 21*** true . /* all conclusions proved */ 22 23 24For path(s) from start to finish: 25 26function_r_r_2. 27H1: j >= 0 . 28H2: j <= 79 . 29H3: block_index__size >= 0 . 30H4: block_index__base__first <= block_index__base__last . 31H5: round_index__size >= 0 . 32H6: round_index__base__first <= round_index__base__last . 33H7: block_index__base__first <= 0 . 34H8: block_index__base__last >= 15 . 35H9: round_index__base__first <= 0 . 36H10: round_index__base__last >= 79 . 37 -> 38C1: 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) . 52C2: 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 . 66C3: 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 82