Post on 07-Sep-2019
Spezifikation von ProgrammenOOPM, Ralf Lämmel
Wer ist denn das?
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Programmspezifikation mit Vor- und Nachbedingungen
301
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Gesprächsprotokoll
302
“Joe the programmer”
“Ed the computer scientist”
Die beiden Leute führen ein Gespräch zur Korrektheit von
Programmen.
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Die Frage nach der Korrektheit
303
q = 0; r = x; while (r > y) { r = r - y; q = q + 1; }
Ich habe hier ein Programm für die Division mit Rest.
Ist dieses Programm korrekt?
“Division mit Rest” ist zu informal.
Können Sie das formaler ausdrücken?
Was ist also die Spezifikation für Ihr Programm?
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Keine Korrektheit ohne Spezifikation
304
Das Programm soll den Quotient q und den Rest r für die Division der natürlichen Zahlen x und y berechnen.
Haben Sie diese Spezifikation (Nachbedingung) im Sinn?
{ x == y ∗ q + r }
q = 0; r = x; while (r > y) { r = r - y; q = q + 1; }
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Programm mit Spezifikation
305
q = 0; r = x; while (r > y) { r = r - y; q = q + 1; }
{ x == y ∗ q + r }Es ist dies zu zeigen:
Nachbedingung
Nach Programmausführung
gilt, dass ...
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Zu schwache Vorbedingung
306
Das Programm ist nicht korrekt!
Es terminiert nicht für y = 0.
Terminieren soll es also auch? Sie sollten die Vorbedingung aufnehmen dass y > 0.
q = 0; r = x; while (r > y) { r = r - y; q = q + 1; }
{ x == y ∗ q + r }
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Programm mit Spezifikation V2
307
q = 0; r = x; while (r > y) { r = r - y; q = q + 1; }
{ x == y ∗ q + r }
{ y > 0 }
Zusicherungen
Angenommen:
Dann ist dies zu zeigen:
Nachbedingung
Vorbedingung
Vor Programmausführung muss gelten, dass ...
Nach Programmausführung
gilt, dass ...
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Zu schwache Nachbedingung + Bug
308
Sie wollen vielleicht, dass r < y am Programmende gilt. Ich kann Korrektheit dafür nicht beweisen. Ihre Schleifenbedingung schaut komisch aus.
q = 0; r = x; while (r > y) { r = r - y; q = q + 1; }
Für x = 6 und y = 3 berechnet es q = 1 und r = 3 anstatt q = 2 und r = 0.
{ y > 0 }
{ x == y ∗ q + r }
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 309
q = 0; r = x; while (r >= y) { r = r - y; q = q + 1; }
{ x == y ∗ q + r && r < y }
{ y > 0 }
Programm mit Spezifikation V3
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Unterspezifikation
310
Sie solten wenigstens negative Werte ausschließen. Eventuell wollen Sie das Programm verallgemeinern.
q = 0; r = x; while (r >= y) { r = r - y; q = q + 1; }
Ich möchte das Programm mit Datentyp int implementieren. Muss ich dazu Anpassungen vornehmen?
{ y > 0 }
{ x == y ∗ q + r && r < y }
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 311
q = 0; r = x; while (r >= y) { r = r - y; q = q + 1; }
{ x >= 0 && y > 0 }
Programm mit Spezifikation V4
{ x == y ∗ q + r && r < y && r >= 0 && q >= 0 }
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Was tun? (mit den Spezifikationen)
312
Dokumentation
Überprüfen der Bedingungen zur Laufzeit
Verifizieren der Bedingungen vor Laufzeit
Ableitung einer Implementation aus Spezifikation
Verwendung der Spezifikation zur Testdatengenerierung
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 313
Programm ohne Spezifikation
// Variable declarations and test dataint x = 6;int y = 3;int q;int r;
// The actual program (algorithm)q = 0;r = x;while (r >= y) {
r = r - y;q = q + 1;
}
// Print the resultSystem.out.println( x + " = " + y + " * " + q + " + " + r);
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 314
Programm mit Zusicherungen
... // Preconditionassert x >= 0 && y > 0;
// The actual program (algorithm)q = 0;r = x;while (r >= y) {
r = r - y;q = q + 1;
}
// Postconditionassert x == y * q + r && r < y && r >= 0 && q >= 0;...
Java’sZusicherungen(“Assertions”) werden zur
Laufzeit geprüft.
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Java’s assert
Anweisungsform:assert BoolescherAusdruck;
Zur Laufzeit:Berechne Ausdruck.Wirf Ausnahme wenn das Resultat false ist.
Beachte:Überprüfung verlangt VM Parameter:
-enableassertions
315
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 316
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Verwendung von Spezifikationen für Laufzeitüberprüfungen
317
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Beispiel: Korrektheit von BubbleSort
318
Gegeben ist die Sortiermethode:
static void bubbleSort(int[] a) { ... }
Ist diese Methode korrekt?
Was ist das Korrektheitskriterium?
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Korrektheit des Sortieralgorithmus
Für alle int[] a, b,
wobei a und b Klone voneinander sind,
gilt nach der Ausführung von bubbleSort(a),
dass:
isSorted(a)und
isPermutation(a,b)
319
Die Formulierung würde sich ändern, wenn bubbleSort ohne
Seiteneffekte arbeitete.
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Kontrollierende Anwendung von BubbleSort
320
int[] b = a.clone();bubbleSort(a);assert isSorted(a) && isPermutation(a,b);
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Verschieben der Zusicherungen in die Methode zum Sortieren
321
public static void bubbleSort(int[] a) {int[] b = a.clone();boolean swapped; // to notice swaps during a passdo {
swapped = false;for (int i = 1; i < a.length; i++)
if (a[i - 1] > a[i]) {// Swap!int swap = a[i];a[i] = a[i - 1];a[i - 1] = swap;swapped = true;
}} while (swapped); // another pass if swaps happenedassert isSorted(a) && isPermutation(a,b);
}
Das Ausschalten von „assert“ vermeidet nicht
das Klonen. Wir kann man dies ändern?
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Beispiel: Korrektheit von Suchverfahren
Relevante AlgorithmenLineare Suche (mit Indexrückgabe)
Binäre Suche (mit Indexrückgabe)
Erfassung des Fortschritts der Suche.
Verwendung einer einfachen Hilfseigenschaft.public static boolean member(
int[] a, int x, -- Reguläre Eingabe
int from, int to) -- Einschränkung der Indizes322
Hier erfassen wir keine allgemeinen Vor- und
Nachbedingungen sondern andere Eigenschaften an
verschiedenen Stellen des Programms.
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 323
/**
* @param a an array to search for x
* @param x the element to search in a
* @param from the start index of a for the window of searching
* @param to the end index of a for the window of searching
* @return Boolean to say whether x is a member of a
*/
public static boolean member(int[] a, int x, int from, int to) {
for (int i=from; i<=to; i++)
if (a[i]==x)
return true;
return false;
}
Hilfsmethode zur Benutzung in
Spezifiaktionen. (Was ist wenn
diese Methode “falsch” ist?)
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 324
Lineare Suche ohne Zusicherungen
public static int linear(int[] a, int x) {for (int i=0; i<a.length; i++)
if (a[i] == x) return i;
return -1;}
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 325
Lineare Suche mit Zusicherungenpublic static int linear(int[] a, int x) {
for (int i=0; i<a.length; i++) {assert !member(a,x,0,i-1);if (a[i] == x) {
assert member(a,x,i,i);assert member(a,x,0,a.length-1);return i;
}assert !member(a,x,0,i);
}assert !member(a,x,0,a.length-1);return -1;
}
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau 326
Binäre Suche ohne Zusicherungenpublic static int binary(int[] a, int x) {
int first = 0;int last = a.length - 1;while (first <= last) {
int middle = first + ((last - first) / 2);if (a[middle] < x) {
first = middle + 1;} else if (a[middle] > x) {
last = middle - 1;} else
return middle;}return -1;
}
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
public static int binary(int[] a, int x) {int first = 0;int last = a.length - 1;while (first <= last) {
int middle = first + ((last - first) / 2);if (a[middle] < x) {
assert !member(a,x,first,middle);first = middle + 1;
} else if (a[middle] > x) {assert !member(a,x,middle,last);last = middle - 1;
} elsereturn middle;
}assert !member(a,x,0,a.length-1);return -1;
}327
Binäre Suche mit Zusicherungen
(C) Ralf Lämmel, OOPM, Universität Koblenz-Landau
Zusammenfassung Programme mit Spezifikationen
Vor-, Nach- und „Zwischen-“ BedingungenLaufzeitüberprüfung von Spezifikationen
Auch Assertion-basiertes DebuggingAusblick
Tests als SpezifikationenStatische Verifikation von Spezifikationen