Algorithmus	Einführung Definition Definitionen Flussdiagramme Struktogramme Korrektheit Verifikation Testen Rekursion Literatur Standard-Algorithmen Numerik Links Pfad: Startseite / Fächer / Informatik / Algorithmus / Verifikation
Autor: mk 06.12.2005 13:52 2971	Algorithmus

Formale Verifikation am Beispiel der ägyptischen Bauern-Multiplikation

Es ist aus der Gültigkeit der Vorbedingung die Gültigkeit der Nachbedingung zu zeigen. Aus der Zusicherung {z + x*y = a*b und a,b >= 0} folgt die Gültigkeit der Schleifeninvariante { z + x*y = a*b } zu Beginn der Schleife.

Wir zeigen, dass die Schleifeninvariante nach Durchlaufen des Schleifenkörpers invariant bleibt. Die Werte der Variablen x,y,z nach Durchlaufen des Schleifenkörpers nennen wir x',y',z'.

Es gibt zwei Fälle:

1. x ist ungerade
   
   z' = z+y; y' = 2*y; 2*x'+1=x bzw. x' = (x-1)/2;
   =>
   z' + x'*y' = z+y + (x-1)/2 * 2*y = z+y + (x-1)*y = z+y + x*y - y = z + x*y .
   
   
2. x ist gerade
   
   z' = z; y' = 2*y; x' = x/2;
   =>
   z' + x'*y' = z + x/2 * 2*y = z + x*y.

Die while-Schleife terminiert sicher (kommt zu einem Ende), da x ganzzahlig halbiert wird.
Damit ist formal bewiesen, dass der Algorithmus tatsächlich das Produkt liefert.

Bemerkung:

Der Algorithmus hat eine große Bedeutung für das binäre Multiplizieren, denn im Binär-System ist das Multiplizieren mit 2 und das Dividieren durch 2 so einfach wie das Multiplizieren mit 10 und das Dividieren durch 10 im Zehner-System. Ebenso muss man sich, um festzustellen, ob eine Zahl ungerade ist, nur ein Bit ansehen.

Aufgabe:

Der Programm-Abschnitt

x := a; y := b; p := 0;
while x > 0 do
begin
  p := p+y;
  x := x-1;
end;

beschreibt einen Algorithmus.

Überlege, was die Ein- und Ausgaben sein könnten und was der Algorithmus tut.

Beschreibe den Algorithmus informell in einem Satz.

Beweise formal durch Zusicherung deine Angaben.

Zeichne ein Struktogramm einschließlich der Zusicherungen.

lokal