Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
s_r.siv
Sprache: Unknown
Haftungsausschluß.siv KontaktHlasm {Hlasm[738] BAT[808] Abap[928]}diese Dinge liegen außhalb unserer Verantwortung
*****************************************************************************
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:30
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
function RMD.S_R
For path(s) from start to run-time check associated with statement of line 101:
function_s_r_1.
*** true . /* all conclusions proved */
For path(s) from start to finish:
function_s_r_2.
H1: j >= 0 .
H2: j <= 79 .
H3: integer__size >= 0 .
H4: round_index__size >= 0 .
H5: round_index__base__first <= round_index__base__last .
H6: rotate_amount__size >= 0 .
H7: round_index__base__first <= 0 .
H8: round_index__base__last >= 79 .
->
C1: element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] :=
8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] :=
9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] :=
9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] :=
6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] :=
15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] :=
12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46]
:= 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52]
:= 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58]
:= 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64]
:= 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70]
:= 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76]
:= 15, [77] := 13, [78] := 11, [79] := 11), [j]) = s_r_spec(j) .
C2: element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] :=
8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] :=
9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] :=
9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] :=
6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] :=
15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] :=
12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46]
:= 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52]
:= 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58]
:= 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64]
:= 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70]
:= 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76]
:= 15, [77] := 13, [78] := 11, [79] := 11), [j]) >= 0 .
C3: element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] :=
8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] :=
9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] :=
9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] :=
6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] :=
15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] :=
12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46]
:= 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52]
:= 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58]
:= 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64]
:= 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70]
:= 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76]
:= 15, [77] := 13, [78] := 11, [79] := 11), [j]) <= 15 .
[ Seitenstruktur1.307Drucken
]
|
|
