Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
cfscript.xml
Sprache: XML
Untersuchungsergebnis.siv Download desHlasm {Hlasm[669] BAT[743] Abap[859]}zum Wurzelverzeichnis wechseln
*****************************************************************************
Semantic Analysis of SPARK Text
Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
*****************************************************************************
CREATED 29-NOV-2010, 14:30:19 SIMPLIFIED 29-NOV-2010, 14:30:28
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
function RMD.R_L
For path(s) from start to run-time check associated with statement of line 59:
function_r_l_1.
*** true . /* all conclusions proved */
For path(s) from start to finish:
function_r_l_2.
H1: j >= 0 .
H2: j <= 79 .
H3: block_index__size >= 0 .
H4: block_index__base__first <= block_index__base__last .
H5: round_index__size >= 0 .
H6: round_index__base__first <= round_index__base__last .
H7: block_index__base__first <= 0 .
H8: block_index__base__last >= 15 .
H9: round_index__base__first <= 0 .
H10: round_index__base__last >= 79 .
->
C1: element(mk__block_permutation([0] := 0, [1] := 1, [2] := 2, [3] := 3, [4]
:= 4, [5] := 5, [6] := 6, [7] := 7, [8] := 8, [9] := 9, [10] := 10, [
11] := 11, [12] := 12, [13] := 13, [14] := 14, [15] := 15, [16] := 7,
[17] := 4, [18] := 13, [19] := 1, [20] := 10, [21] := 6, [22] := 15, [
23] := 3, [24] := 12, [25] := 0, [26] := 9, [27] := 5, [28] := 2, [29]
:= 14, [30] := 11, [31] := 8, [32] := 3, [33] := 10, [34] := 14, [35]
:= 4, [36] := 9, [37] := 15, [38] := 8, [39] := 1, [40] := 2, [41]
:= 7, [42] := 0, [43] := 6, [44] := 13, [45] := 11, [46] := 5, [47]
:= 12, [48] := 1, [49] := 9, [50] := 11, [51] := 10, [52] := 0, [53]
:= 8, [54] := 12, [55] := 4, [56] := 13, [57] := 3, [58] := 7, [59]
:= 15, [60] := 14, [61] := 5, [62] := 6, [63] := 2, [64] := 4, [65]
:= 0, [66] := 5, [67] := 9, [68] := 7, [69] := 12, [70] := 2, [71] :=
10, [72] := 14, [73] := 1, [74] := 3, [75] := 8, [76] := 11, [77] :=
6, [78] := 15, [79] := 13), [j]) = r_l_spec(j) .
C2: element(mk__block_permutation([0] := 0, [1] := 1, [2] := 2, [3] := 3, [4]
:= 4, [5] := 5, [6] := 6, [7] := 7, [8] := 8, [9] := 9, [10] := 10, [
11] := 11, [12] := 12, [13] := 13, [14] := 14, [15] := 15, [16] := 7,
[17] := 4, [18] := 13, [19] := 1, [20] := 10, [21] := 6, [22] := 15, [
23] := 3, [24] := 12, [25] := 0, [26] := 9, [27] := 5, [28] := 2, [29]
:= 14, [30] := 11, [31] := 8, [32] := 3, [33] := 10, [34] := 14, [35]
:= 4, [36] := 9, [37] := 15, [38] := 8, [39] := 1, [40] := 2, [41]
:= 7, [42] := 0, [43] := 6, [44] := 13, [45] := 11, [46] := 5, [47]
:= 12, [48] := 1, [49] := 9, [50] := 11, [51] := 10, [52] := 0, [53]
:= 8, [54] := 12, [55] := 4, [56] := 13, [57] := 3, [58] := 7, [59]
:= 15, [60] := 14, [61] := 5, [62] := 6, [63] := 2, [64] := 4, [65]
:= 0, [66] := 5, [67] := 9, [68] := 7, [69] := 12, [70] := 2, [71] :=
10, [72] := 14, [73] := 1, [74] := 3, [75] := 8, [76] := 11, [77] :=
6, [78] := 15, [79] := 13), [j]) >= 0 .
C3: element(mk__block_permutation([0] := 0, [1] := 1, [2] := 2, [3] := 3, [4]
:= 4, [5] := 5, [6] := 6, [7] := 7, [8] := 8, [9] := 9, [10] := 10, [
11] := 11, [12] := 12, [13] := 13, [14] := 14, [15] := 15, [16] := 7,
[17] := 4, [18] := 13, [19] := 1, [20] := 10, [21] := 6, [22] := 15, [
23] := 3, [24] := 12, [25] := 0, [26] := 9, [27] := 5, [28] := 2, [29]
:= 14, [30] := 11, [31] := 8, [32] := 3, [33] := 10, [34] := 14, [35]
:= 4, [36] := 9, [37] := 15, [38] := 8, [39] := 1, [40] := 2, [41]
:= 7, [42] := 0, [43] := 6, [44] := 13, [45] := 11, [46] := 5, [47]
:= 12, [48] := 1, [49] := 9, [50] := 11, [51] := 10, [52] := 0, [53]
:= 8, [54] := 12, [55] := 4, [56] := 13, [57] := 3, [58] := 7, [59]
:= 15, [60] := 14, [61] := 5, [62] := 6, [63] := 2, [64] := 4, [65]
:= 0, [66] := 5, [67] := 9, [68] := 7, [69] := 12, [70] := 2, [71] :=
10, [72] := 14, [73] := 1, [74] := 3, [75] := 8, [76] := 11, [77] :=
6, [78] := 15, [79] := 13), [j]) <= 15 .
[ zur Elbe Produktseite wechseln0.136Quellennavigators
]
|
|
