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