Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Unknown

Columbo aufrufen.siv zum Wurzelverzeichnis wechselnHlasm {Hlasm[669] BAT[745] Abap[861]}Datei anzeigen

*****************************************************************************
                       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:21

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_R

For path(s) from start to run-time check associated with statement of line 73:

function_r_r_1.
*** true .          /* all conclusions proved */

For path(s) from start to finish:

function_r_r_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] := 5, [1] := 14, [2] := 7, [3] := 0, [
          4] := 9, [5] := 2, [6] := 11, [7] := 4, [8] := 13, [9] := 6, [10] :=
          15, [11] := 8, [12] := 1, [13] := 10, [14] := 3, [15] := 12, [16] :=
          6, [17] := 11, [18] := 3, [19] := 7, [20] := 0, [21] := 13, [22] :=
          5, [23] := 10, [24] := 14, [25] := 15, [26] := 8, [27] := 12, [28] :=
          4, [29] := 9, [30] := 1, [31] := 2, [32] := 15, [33] := 5, [34] := 1,
          [35] := 3, [36] := 7, [37] := 14, [38] := 6, [39] := 9, [40] := 11, [
          41] := 8, [42] := 12, [43] := 2, [44] := 10, [45] := 0, [46] := 4, [
          47] := 13, [48] := 8, [49] := 6, [50] := 4, [51] := 1, [52] := 3, [53]
           := 11, [54] := 15, [55] := 0, [56] := 5, [57] := 12, [58] := 2, [59]
          := 13, [60] := 9, [61] := 7, [62] := 10, [63] := 14, [64] := 12, [65]
          := 15, [66] := 10, [67] := 4, [68] := 1, [69] := 5, [70] := 8, [71]
          := 7, [72] := 6, [73] := 2, [74] := 13, [75] := 14, [76] := 0, [77]
          := 3, [78] := 9, [79] := 11), [j]) = r_r_spec(j) .
C2:    element(mk__block_permutation([0] := 5, [1] := 14, [2] := 7, [3] := 0, [
          4] := 9, [5] := 2, [6] := 11, [7] := 4, [8] := 13, [9] := 6, [10] :=
          15, [11] := 8, [12] := 1, [13] := 10, [14] := 3, [15] := 12, [16] :=
          6, [17] := 11, [18] := 3, [19] := 7, [20] := 0, [21] := 13, [22] :=
          5, [23] := 10, [24] := 14, [25] := 15, [26] := 8, [27] := 12, [28] :=
          4, [29] := 9, [30] := 1, [31] := 2, [32] := 15, [33] := 5, [34] := 1,
          [35] := 3, [36] := 7, [37] := 14, [38] := 6, [39] := 9, [40] := 11, [
          41] := 8, [42] := 12, [43] := 2, [44] := 10, [45] := 0, [46] := 4, [
          47] := 13, [48] := 8, [49] := 6, [50] := 4, [51] := 1, [52] := 3, [53]
           := 11, [54] := 15, [55] := 0, [56] := 5, [57] := 12, [58] := 2, [59]
          := 13, [60] := 9, [61] := 7, [62] := 10, [63] := 14, [64] := 12, [65]
          := 15, [66] := 10, [67] := 4, [68] := 1, [69] := 5, [70] := 8, [71]
          := 7, [72] := 6, [73] := 2, [74] := 13, [75] := 14, [76] := 0, [77]
          := 3, [78] := 9, [79] := 11), [j]) >= 0 .
C3:    element(mk__block_permutation([0] := 5, [1] := 14, [2] := 7, [3] := 0, [
          4] := 9, [5] := 2, [6] := 11, [7] := 4, [8] := 13, [9] := 6, [10] :=
          15, [11] := 8, [12] := 1, [13] := 10, [14] := 3, [15] := 12, [16] :=
          6, [17] := 11, [18] := 3, [19] := 7, [20] := 0, [21] := 13, [22] :=
          5, [23] := 10, [24] := 14, [25] := 15, [26] := 8, [27] := 12, [28] :=
          4, [29] := 9, [30] := 1, [31] := 2, [32] := 15, [33] := 5, [34] := 1,
          [35] := 3, [36] := 7, [37] := 14, [38] := 6, [39] := 9, [40] := 11, [
          41] := 8, [42] := 12, [43] := 2, [44] := 10, [45] := 0, [46] := 4, [
          47] := 13, [48] := 8, [49] := 6, [50] := 4, [51] := 1, [52] := 3, [53]
           := 11, [54] := 15, [55] := 0, [56] := 5, [57] := 12, [58] := 2, [59]
          := 13, [60] := 9, [61] := 7, [62] := 10, [63] := 14, [64] := 12, [65]
          := 15, [66] := 10, [67] := 4, [68] := 1, [69] := 5, [70] := 8, [71]
          := 7, [72] := 6, [73] := 2, [74] := 13, [75] := 14, [76] := 0, [77]
          := 3, [78] := 9, [79] := 11), [j]) <= 15 .

[ Original von:0.683Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt. ]