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

Code:

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

		int a = 0 ;
		int i = n ;

		while ( i > 0 )
		{
			a = 2 * a + 1;
			i--;
		}

		// Ende

		return a;
	}


Zu zeigen:  { n >= 0 } c { a = p(n) }

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


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

2.) Schleifen-Invariante:


	Tabelle fŸr n = 5:

	|    i |  5 |  4 |  3 |  2 |  1 |  0 |
	--------------------------------------
	|    a |  0 |  1 |  3 |  7 | 15 | 31 |
	--------------------------------------
        |  n-i |  0 |  1 |  2 |  3 |  4 |  5 |
	--------------------------------------
        | p(i) | 31 | 15 |  7 |  3 |  1 |  0 |


	Invariante I = ( pow (2, n-i) * p(i) + a = p(n) ) ^ (n >= i) ^ (i >= 0)

	Beispiel zur Tabelle fŸr i = 3: pow (2, 2) * 7 + 3 = 4 * 7 + 3 = 31

	Mit pow (2, n-i) ist "2 hoch (n-i)" gemeint. Das Hausdach ^ kommt nicht zum Einsatz,
	da es bereits als logisches UND verwendet wird.

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


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


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


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

    { n >= 0 } a := 0; i := n { n >= 0 ^ a = 0 ^ i = n }        { n >= 0 ^ a = 0 ^ i = n } while (i > 0) { a = 2 * a + 1; i-- } { a = p(n) }
  -------------------------------------------------------------------------------------------------------------------------------------------- H-SEQ
                            { n >= 0 }        a := 0; i := n; while (i > 0) { a = 2 * a + 1; i-- }          { a = p(n) }


Beweis fŸr [X]:

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

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

	p(n)  = pow (2, n-i) * p(i) + a =
	      = pow (2, n-n) * p(n) + a =
	      =       1      * p(n) + 0 =
	      =                p(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 a = p(n) erfŸllt wird.

	Es gelte die Invariante wie oben definiert. Diese schreibt unter anderem vor, dass i >= 0.
	Au§erdem sei nun i <= 0, da dies die Negation von b darstellt (denn b = i > 0) Schleifenabbruchbedingung).

	Damit muss i = 0 sein.

	Zu zeigen ist, dass dies alles zu a = p(n) fŸhrt.

	p(n)  = pow (2, n-i) * p(i) + a =
	      = pow (2, n)   * p(0) + a =
	      = pow (2, n)   *  0   + a =
	      =                       a

	Also liegt in a tatsŠchlich der Wert von p(n). Die Korrektheit ist fŸr { n >= 0 } bewiesen.