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

  • Kannst du die Angabe so abschreiben, dass man alle Symbole hat? Außerdem ist die Ausgabe nicht "i", sondern "u". Hast du vielleicht sonst noch Fehler gemacht? Soll das unter dem Code eine Schleifeninvariante sein? Formatierung in einer CODE-Umgebung würde der Lesbarkeit auch nicht schaden.

    Dipper dipper dii dipper dii dipper dii duuu

  • Wer hat das bitte geschrieben? Hoffentlich kein Prof. Das ist nach wie vor voll von Fehlern.

    Z.B. Ausgabe heißt oben immer noch "i", unten dann "u"; "u = -1" sollte heißen "u := -1".

    Naja, dann füg halt mal ein.
    Vorbedingungen: a >= 0, n >= 0, b >= 0
    Nachbedingung: u >= -1
    Und dann Zeile für Zeile durchbeweisen.

    Die ersten ganz einfach mit der Statementregel:
    {P} u := -1 {P'}
    {P'} y := x+y {P''}
    {P''}......
    ...... {Q}

    Die Schleifeninvariante ist auch gegeben (muss man normal mühsam finden). Einfach mit der Schleifenregel schauen, obs passt.

    Für If-Verzweigungen gibt es auch eine eigene Regel.

    Dipper dipper dii dipper dii dipper dii duuu

Jetzt mitmachen!

Sie haben noch kein Benutzerkonto auf unserer Seite? Registrieren Sie sich kostenlos und nehmen Sie an unserer Community teil!