Leonhard Fellermayr
Info II - Schriftliche Aufgabe S-12 (Fakultaet.txt) - Beweis im Hoare-KalkŸl

Code:

	public static int fakultaet (int n)
	{
		// Anfang

		int a = 1;
		int k = n;

		while (k > 0)
		{
			a = a * k;
			k--;        /* k = k - 1 */
		}

		// Ende

		return a;
	}


Zu zeigen:  { n >= 0 } c { a = n! }

1.) ZunŠchst Beweis der beiden Zuweisungen vor Beginn der Schleife: jeweils H-ASS, Komposition per H-SEQ


     true => (a = 1) [ a := 1 ] = (a = 1)                   a = 1 => (a = 1) ^ (k = n) [ k := n ] = (k = n)
   ---------------------------------------- H-ASS       -------------------------------------------------------- H-ASS
     { n >= 0 } a := 1 { n >= 0 ^ a = 1 }                 { n >= 0 ^ a = 1 } k := n { n >= 0 ^ a = 1 ^ k = n }
 ----------------------------------------------------------------------------------------------------------------------- H-SEQ
(*)                                 { n >= 0 } a := 1; k := n { n >= 0 ^ a = 1 ^ k = n }

2.) Schleifen-Invariante:

	I = (a * k! = n!) ^ (k >= 0)


3.) Beweis der Anweisungen im Schleifenrumpf: 2x H-ASS, Komposition via H-SEQ


               I ^ (k > 0) => a := a * k                           I ^ (k > 0) => k := k - 1
      -------------------------------------------- H-ASS     -------------------------------------- H-ASS
       { I ^ (k > 0) } a := a * k { I ^ (k > 0) }               { I ^ (k > 0) } k := k - 1 { I }
    ------------------------------------------------------------------------------------------------------ H-SEQ
(**)                               { I ^ (k > 0) } a := a * k; k := k - 1 { I }


4.) Jetzt Einbettung von (**) in H-WHILE:
                                                                  ( Beweis unten [X] )         ( Beweis unten [XX] )
         { I ^ (k > 0) } a := a * k; k := k - 1 { I }          n >= 0 ^ a = 1 ^ k = n => I     I ^ (k <= 0) => a = n!
    -------------------------------------------------------------------------------------------------------------------- H-WHILE
(***)                      { n >= 0 ^ a = 1 ^ k = n } while (k > 0) { a = a * k; k-- } { a = n! }


Sequentialisiere nun letztendlich die sequentialisierten Zuweisungen (*) und die Schleife (***):

    { n >= 0 } a := 1; k := n { n >= 0 ^ a = 1 ^ k = n }           { n >= 0 ^ a = 1 ^ k = n } while (k > 0) { a = a * k; k-- } { a = n! }
  ------------------------------------------------------------------------------------------------------------------------------------------ H-SEQ
                                    { n >= 0 } a := 1; k := n; while (k > 0) { a = a * k; k-- } { a = n! }


Beweis fŸr [X]:

	Diese Vorbedingung stellt sicher, dass die Invariante bereits VOR der SchleifenausfŸhrung gegolten hat.

	FŸr a = 1 und k = n (wobei n >= 0 als Ursprungsbedingung) ist

		a * k! = n!
	nŠmlich	1 * k! = n!
	oder	1 * n! = n!	(wegen k = n)

	Da dies wahr ist, galt die Invariante vor dem ersten Schleifendurchlauf bereits.

Beweis fŸr [XX]:

	Diese Zuweisung stellt sicher, dass bei Beendigung der Schleife (aufgrund NOT b) immer noch die
	Invariante gilt und desweiteren die Nachbedingung erfŸllt wird.

	Es gelte die Invariante, d. h. a * k! = n!, au§erdem fordert die Invariante k >= 0.
	Des weiteren sei nun k <= 0, da dies die Negation von b darstellt (denn b = (k > 0) Schleifenabbruchbedingung).

	Aus k >= 0 (wegen I) und k <= 0 (wegen NOT b) folgt k = 0. Dann ist aber

		a * k! = n!
	   <=>  a * 0! = n!
	   <=>  a * 1  = n!
	   <=>  a      = n!

	Also gilt tatsŠchlich die Nachbedingung - das ProgrammstŸck tut genau das, was es soll.

Bemerkung:

	†brigens gibt dieses ProgrammstŸck bei einer "bšswilligen" Eingabe (z. B. n := -5)
	fŠlschlicherweise a = 1 != n! zurŸck, da die Schleife gar nicht ausgefŸhrt wird (b = false schon
	zu Beginn). Aber der Korrektheitsbeweis sollte ja ohnehin unter der Vorbedingung { n >= 0 }
	gefŸhrt werden. FŸr andere Eingaben liefert das Programm kein korrektes Ergebnis.