Sei, wie in der Angabe, c der Programmteil zwischen // Anfang  und //
Ende, und s die while-Schleife

Wir sollen herleiten:

    1 : { n >= 0 } c { a == 2^n-1 } 

1 folgt mittels (H-SEQ) aus 2 und 7.

    2 : { n >= 0 } a=0 ; i=n ; { n >= 0  &  a == 0  & i == n } 

2 folgt mittels (H-SEQ) aus 3 und 5.

    3 : { n >= 0 } a=1; { n >= 0  &  a == 0 } 

3 folgt mittels (H-ASS) aus 4 

    4 :  n >= 0  -> ( n >= 0  &  1 == 1 )   


    5 : { n >= 0  &  a == 0 } i=n; { n >= 0  &  a == 0  & i == n } 

5 folgt mittels (H-ASS) aus 6 

    6 : ( n >= 0  &  a == 1 ) -> ( n >= 0  &  a == 1  & n == n )

 
    7 :  { n >= 0  &  a == 0  & i == n } s { a = 2^n-1 } 

7 folgt mittels (H-WHILE) aus 8, 9 und 10, wobei die Invariante
I ist:  ( i >= 0  &  a == 2^(n-i)-1 ) )

    8 :  ( n >= 0  &  a == 1  & i == n ) -> I 

8 gilt, wie man durch einsetzen errechnet. 


    9 :  ( I & i <= 0 )  ->  ( a == 2^n-1 ) 

9 gilt, da aus I und i <= 0 folgt i==0, und somit 
a == 2^(n-i)-1 == 2^n-1  gilt.


   10 :  { I & i > 0 } a = 2*a+1 ; i = i-1 ; { I } 

10 folgt mittels (H-SEQ) aus 11 und 12  

   11 :  { a == 2^{n-i+1}+1  &  i >= 1 } i = i-1 ; { I } 

Da die Vorbedingung nichts anderes ist als I[ i := (i-1) ], folgt 
11 trivialerweise mittels (H-ASS)  


   12 :  { I & i > 0 } a = 2*a+1 ; { a == 2^(n-i+1)+1  &  i >= 1 }  

12 folgt mittels (H-ASS) aus 13 

   13 :  ( I & i > 0 ) ->  2*a+1 == 2^(n-i+1)-1  &  i >= 1 ) 

Das zweite Konjunktionsglied  i >= 1 folgt aus i > 0, da i 
vom Typ int ist. Das erste, 2*a+1 == (2^(n-i+1)-1)+1 , 
erhaelt man durch ausrechnen aus I, da gilt:
 2*a+1 == 2*(2^(n-i)-1)+1 == 2^(n-i+1)-2 +1 == 2^(n-i+1)-1