Hoarekalkül
Aus Infostudium Wiki
| Dieser Artikel soll in Zukunft noch erweitert bzw. überarbeitet werden. Dies soll aber nicht als Reservierung aufgefasst werden. Mitarbeit ist erwünscht. |
Inhaltsverzeichnis |
Allgemein
ein umfangreiches Tutorial: Der Umgang mit dem Hoare-Kalkül zur Programmverifikation
Beispiele
Beispiel 1
Hier ein Beispiel für eine Verifikation eines Programms, das eine Zahl zum Quadrat berechnet. Diese Beispiel wurde aus einer Probeklausur entnommen, die freundlicherweise von dem Tutor Thomas (Gruppe 4) erstellt wurde.
Die Kommentare sollen einem helfen, die Gedankengänge zu verstehen. Die obligatorischen und-Verknüpfungszeichen wurden durch && ersetzt.
Das Problem ist, dass die Klausur-Steller es so gedreht haben, dass es nur für die Schleifeninvariante oder komplette Teile Punkte gibt. Daher lautet die Devise: Nur machen, wenn man es komplett macht.
Aufgabenstellung:
Beweisen Sie die partielle Korrektheit dieses Programms, d.h. aus der Vorbedingung < true > soll die Nachbedingung < square = n2 > folgen.
< true > // Wie üblich erst mal mit der Startbedingung anfangen.
< k = k > // Hier wurde anscheinend vorrausgedacht: Um der Variable k einen Wert zuweisen zu können, wird der Ausdruck k=k hingeschrieben. n wurde nicht berücksichtigt (?).
if (n < 0) {
< k = k && n < 0 > // Bedingungen werden einfach hinten dran gehängt (hoffe, das gibt Punkte)
k = -n;
< k = −n && n < 0 > // Nun konnte der Variable k der Wert von n zugewiesen werden.
< k = |n| > // Nun wurde mathematische Vereinfachung durchgeführt. Scheint anscheinend machbar zu sein.
} else {
< k = k ^ n >= 0 > // Und wieder eine Bedingung. Also dranhängen.
k = n; // wie oben
< k = n ^ n >= 0 > // wie oben
< k = |n| > // wie oben
}
< k = |n| > // ok, k ist der Betrag von n. Ergebnis des ganzen If-Prozedur-Krams
< 0 + (k − 0)k = k^2 && 0 <= k && k = |n| > // Und jetzt geht der Spaß erst richtig los: "k=|n|" mitschleifen, ist klar.
Normalerweise wird ja mit der Nachbedingung angefangen. Dies wurde hier auch getan, aber es wurde schon die linke Seite erweitert um eine 0 durch square ersetzen zu können. Direkt mit "0 + (k − 0)k" anzufangen ist etwas kompliziert. Der Autor hat anscheinend schonmal die Schleifeninvariante gesucht.
square = 0;
< square + (k − 0)k = k^2 && 0 <= k && k = |n| > // ok, 0 durch square ersetzt.
i = 0;
< square + (k − i)k = k^2 && 0 <= k && k = |n| > // Nun zeigt sich, warum der Autor schon vorher "k-0" eingebaut hatte.
while (i < k) {
< square + (k − i)k = k^2 && 0 <= k && k = |n| && i < k > // "i < k" ist eine Bedingung, also dranhängen
< square + (k − (i + 1))k + (k − 0) = k^2 && i + 1 <= k && k = |n| && 0 <= k > // Der Autor hat i um 1 erhöht, dadurch konnte er das "<" durch "<=" ersetzen. Warum er hier schon allerdings hier schon "i+1" verwendet hat, ist mir nicht ganz schlüssig. Hier wurde zudem noch die nächste Schleifeninvariante eingebaut. Die Frage, die man sich hier stellen muss, ist, was kann man verändern, um aber trotzdem noch auf k^2 zu kommen bzw. was sich verändert, um sich k^2 zu nähern.
j = 0;
< square + (k − (i + 1))k + (k − j) = k^2 && i + 1 <= k && k = |n| && j <= k > // 0 durch j ersetzen (wie üblich)
while (j < k) {
< square + (k − (i + 1))k + (k − j) = k^2 && i + 1 <= k && k = |n| && j <= k && j < k > // Bedingung dranhängen
< square + 1 + (k − (i + 1))k + (k − (j + 1)) = k^2 && i + 1 <= k && k = |n| && j + 1 <= k > // Vorbereitung, um sqare + 1 ersetzen zu können. "j <= k && j < k" kann man vereinfachen.
square = square + 1;
< square + (k − (i + 1))k + (k − (j + 1)) = k^2 && i + 1 <= k && k = |n| && j + 1 <= k >
j = j + 1;
< square + (k − (i + 1))k + (k − (j)) = k^2 && i + 1 <= k && k = |n| && j <= k >
}
< square + (k − (i + 1))k + (k − (j)) = k^2 && i + 1 <= k && k = |n| && j <= k && j >= k > // Hier ist eine Schleife zuende. Daher muss die Bedingung, die für die Schleife gegolten hat, negiert werden und hinten drangehängt werden.
< square + (k − (i + 1))k = k^2 && i + 1 <= k && k = |n| > // Wenn j <= k und j >= k sind, folgt daraus, dass j = k ist. Daher nun dieser Vereinfachungsschritt.
i = i + 1;
< square + (k − i)k = k^2 && i <= k && k = |n| >
}
< square + (k − i)k = k^2 && i <= k && k = |n| && i >= k > // Negierung der Schleifenbedingung
(< square = k^2 && k = |n| >) // Hier noch kurz ein Zwischenschritt: i <= k && i >= k daraus folgt: i = k. Daher diese drastische Vereinfachung.
< square = n^2 > // k = |n|, also ersetzen.
Fertig.
Beispiel 2
Ein einfaches Beispiel
Vorbedingung: < n >= 0 >
i = 0
res = 0
while (i <= n) {
}
Terminierung
Schleifeninvariante
Die Schleifeninvariante ist eine Bedingung, die immer bei jedem Schleifendurchgang zutrifft.
Um diese zu finden gibt es mehrere Möglichkeiten.
