Inverianten und Verifikation

[shisha]

kann mir einer anhand eines [u]einfachen[/] Beispiels erklären wie das mit (schleifen) Verifikation und Invarianten funktioniert?

Habe leider nicht genug verstanden um genauere Fragen zu stellen...

[Blue-Tiger]

Ok, Ziel der Verifikation ist, dass du beweisen willst, dass der Code auch genau das tut was er will. Du hast also eine Eingabe, und du willst eine bestimmte Ausgabe.

Ursimpelbeispiel: Eine Funktion, welche die Summe der Elemente in einem Array berechnet.

Als Eingabe hast du ein int-Array der Laenge n. Du verlangst vom Aufrufer deiner Funktion, dass er ein gueltiges Array mitgibt, und eine gueltige Laenge. Dafuer garantierst du, dass deine Funktion eine gueltige Summe zurueckliefert:

int array_sum(int* a, size_t n)
{
    int sum = 0;
    size_t i = 0;
    while (i < n)
    {
        sum += a[i];
        ++i;
    }
    return sum;
}

So, dann beweisen wir das mal.

Im Grunde gehst du so vor, dass du jedes Statement des Codes zerlegst. Du weisst z. B. was VOR der Ausfuehrung des Codes gilt (die "Precondition") und du weisst was nachher gelten soll("Postcondition"). Ich schreib das ab jetzt so {Precondition} Statement {Postcondition}.

Ganz billiges Beispiel waer die Zuweisung:
{i = irgend ein beliebiger Wert} i = 4; {i == 4}.

Ueberlegen wir uns mal die Precondition fuer unsere Funktion. Wir verlangen dass a != NULL, und fuer alle 0 < i < n a[i] einen gueltigen Wert beinhaltet (z. B. keine Speicherzugriffsverletzung verursacht, weil a nur 10 Elemente enthaelt aber irgend ein Tepp die Funktion mit n = 100 aufgerufen hat). Wer diese Postcondition nicht einhaelt darf sich dann aber auch nicht beschweren dass unsre Funktion nicht tut was sie soll.

Die Postcondition ist dann eben, dass der Rueckgabewert die Summe der Werte von a[0] bis a[n-1] ist.

Unser Ziel ists jetzt, aus der Precondition & den gegebenen Code zu zeigen, dass wir die Postcondition garantieren koennen. d.h. wir muessen aus der Precondition der Funktion selbst und der Tatsache, dass die Variable 'sum' vor der Schleife den Wert 0 und 'i' auch den Wert 0 enthalten, sowie dem Schleifencode selbst beweisen, dass nach der Schleife sum die Summe aller Arrayelemente bis n ist.

Dazu suchen wir die sog. "Schleifeninvariante". Das ist eine Aussage, der Vor und nach jedem Schleifendurchlauf gilt.

In unserer Schleife z. B. gilt vor jedem Schleifendurchlauf und nach jedem Schleifendurchlauf die Aussage:

"sum ist die Summe aller Elemente von a[0] bis a[i-1]".

Das ist also unsere Schleifeninvariante.

Und jetzt sehen wir sofort: sobal die Bedingung i < n nicht mehr gilt, dann folgt aus

"i == n" und "sum ist die Summe aller Elemente von a[0] bis a[i-1]" ==> "sum ist die Summe aller Elemente von a[0] bis a[n-1]".... TADA, genau das war die Postcondition der Funktion, damit sind wir fertig.

Ich hab jetzt viel Formalitaeten weggelassen und ein paar Sachen vereinfacht (z. B. dass passieren kann dass 'int' womoeglich nicht gross genug ist um die Summe aller Elemente im Array zu enthalten), aber im Grossen und Ganzen war's das