Vorbedingungen Nachbedingungen
| |
V V
=================
Eingangs- | Programm- | Ausgangs-
------------>| |------------>
größen | abschnitt | größen
=================
: :
:..Invarianten..:
Im Zusammenhang mit der Ausführung von bestimmten Programmabschnitten
ist es oft sinnvoll, bestimmte Bedingungen zu formulieren, die eine
notwendige Bedingung für die Korrekheit der Abläufe darstellen:
Vor- und Nachbedingungen sowie Invarianten gehören nicht zum Algorithmus im engeren Sinne. Das heißt, der Algorithmus liefert - wenn "alles gut geht" - auch ohne Prüfung der Bedingungen das gewünschte Ergebnis.
Mit IF - THEN bzw. IF - THEN - ELSE Programmkonstrukten
lassen sich diese Bedingungen ohne weiteres formulieren.
Moderne Programmiersprachen stellen jedoch teilweise spezielle
Sprachkonstrukte zur Verfügung. Der eigentliche Algorithmus und die an ihn
gebundenen Vor- und Nachbedingungen sowie lassen sich somit klar voneinander
trennen, die Lesbarkeit des Programms wird erhöht.
Da es sich bei Zusicherungen "nur" um zusätzliche Prüfungen
handelt, werden die Sprachmittel zu ihrer Umsetzung oft so realisiert,
daß die Prüfungen ausgeschaltet werden können.
Dies kann zum Beispiel durch Compileroptionen geschehen, d.h. der Compiler
ignoriert dann die Prübedingungen, oder durch Optionen, die das
Laufzeitverhalten beeinflussen.
Das Laufzeitverhalten des Programms kann dann wahlweise auf Sicherheit
(z.B. beim Programmtest oder bei kritischen Einsätzen) oder auf
Effektivität ausgerichtet werden.
Der Einsatz von Zusicherungen wird auch als "programming by contract" bezeichnet: Die beteiligten Programmabschnitte gehen einen Kontrakt ein, der unbedingt zu erfüllen ist. Wird ein Programmabschnitt betreten, so kann er sich auf bestimmte Voraussetzungen verlassen. Sind diese nicht gegeben, so wird das Betreten des entsprechenden Programmabschnitts unterdrückt.
Standard Pascal, Extended Pascal
Spezielle Sprachkonstrukte für Zusicherungen sind nicht vorhanden.
Zusicherungen lassen sich jedoch mit Hilfe einfacher Unterprogramme hervorheben:
Variante 1
PROCEDURE Assert(condition: BOOLEAN);
BEGIN
IF ( NOT condition ) THEN
ausnahme_behandlung;
END;
Variante 2
{ Annahme: es existiert ein vor- oder nutzerdefinierter Datentyp STRING }
PROCEDURE Assert(condition: BOOLEAN, message: STRING);
BEGIN
IF ( NOT condition ) THEN
Writeln(message);
END;
XL PascalEs gibt ein spezielles Sprachkonstrukt als Spracherweiterung:
ASSERT bedingung;Bei Verletzung der Bedingung wird ein Laufzeitfehler ausgelöst.
Beispiel:
ASSERT a >= b ;
Beispiel für den Einsatz von Zusicherungen
Berechnung von x * y für nichtnegative, ganzzahlige Werte x und y unter ausschließlicher Nutzung von Addition und Subtraktion:
result := 0;
step := y;
ASSERT result + step*x = x * y;
WHILE step > 0 DO BEGIN
result := result + x;
step := step - 1;
ASSERT result + step*x = x * y; { Invariante }
END;
Bemerkungen:
Das obige Beispiel ließe sich wie folgt realisieren:
PROGRAM assertion(OUTPUT);
PROCEDURE assert(condition: BOOLEAN);
BEGIN
IF NOT condition THEN BEGIN
Writeln('Zusicherung verletzt');
Halt;
END;
END;
FUNCTION mult(x, y: INTEGER) : INTEGER;
VAR result, step : INTEGER;
BEGIN
result := 0;
step := y;
#ifdef DEBUG
assert(result + step*x = x * y);
#endif
WHILE step > 0 DO BEGIN
result := result + x;
step := step - 1;
#ifdef DEBUG
assert(result + step*x = x * y);
#endif
END;
mult := result;
END;
BEGIN
Writeln(mult(22, 2));
END.
In Abhängigkeit davon, ob die symbolische Konstante DEBUG
definiert ist oder nicht, werden die Zusicherungen ausgewertet. Die obige Lösung läßt sich übernehmen, es müssen jedoch die Preprozessor-Anweisungen angepaßt werden.