Beiträge von Hatake

  • Verifikation/Zusicherungen

    Hallo, (poste das mal hier rein)

    ich hab hier ein kleines Problem mit der Verifikation von einem Programm und komme einfach nicht weiter.


    Das Programm soll einen vorgegebenen Speicherbereich nach einem bestimmten Wert durchsuchen:

    Eingabe: a ( Anfangsadresse, ab der gesucht wird )
    n ( Anzahl der zu durchsuchenden Zellen )
    b ( Wert, der gesucht wird ( F[i]=b , andernfalls i=-1))

    Ausgabe: i ( ein Index, an dem b gefunden wird )

    Programm Suche im Array

    (* erwartete Eingabe a ≥ 0, n ≥ 0, b ≥ 0 *)

    READ(x); (* Index des ersten zu durchsuchenden Feldes *)
    READ(y); (* Anzahl der zu durchsuchenden Felder *)
    READ(z); (* gesuchter Wert*)

    u=-1; (* Voreinstellung der Ausgabe: gefundener Index *)
    y=x+y;
    y=y-1; (* Index des letzten zu durchsuchenden Feldes *)

    WHILE y ≥ x DO

    IF F[y] ≥ z THEN

    IF z ≥ F[y] THEN

    u=y;
    y=x;
    END;
    END;

    y =y - 1;
    END

    PRINT(u);

    Es wurde in der Aufgabe eine Hilfestellung für die Schleife gegeben,
    doch damit kann ich irgendwie nicht viel anstellen:

    ( für alle j( ( y < j < n +a) → ( F[j] ≠ b) ) ^ ( ( u ≠ -1 ) → F[u] = b )


    und schon mal danke im voraus

    Hatake