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 == n! } 

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

    2 : { n >= 0 } a=1 ; k=n ; { n >= 0  &  a == 1  & k == n } 

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

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

3 folgt mittels (H-ASS) aus 4 

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


    5 : { n >= 0  &  a == 1 } k=n; { n >= 0  &  a == 1  & k == n } 

5 folgt mittels (H-ASS) aus 6 

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

 
    7 :  { n >= 0  &  a == 1  & k == n } s { a = n! } 

7 folgt mittels (H-WHILE) aus 8, 9 und 10, wobei die Invariante
I ist:  ( k >= 0  &  a * k! == n! )

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

8 gilt, wie man durch einsetzen errechnet. 

    9 :  ( I & k <= 0 )  ->  ( a == n! ) 

9 gilt, da aus I und k <= 0 folgt k==0, somit k! == 1 gilt 
und daher aus a * k! == n! folgt a == n! 

   10 :  { I & k > 0 } a = a * k ; k = k-1 ; { I } 

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

   11 :  { a * (k-1)! == n!  &  k >= 1 } k = k-1 ; { I } 

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


   12 :  { I & k > 0 } a = a * k ; { a * (k-1)! == n!  &  k >= 1 }  

12 folgt mittels (H-ASS) aus 13 

   13 :  ( I & k > 0 ) ->  ( a * k ) * (k-1)! == n!  &  k>= 1 ) 

Das zweite Konjunktionsglied  k >= 1 folgt aus k > 0, da k 
vom Typ int ist. Das erste, ( a * k ) * (k-1)! = n! , 
erhaelt man durch ausrechnen aus I, da 
 (a * k) * (k-1)! == a * ( k * (k-1)! ) == a * k!  ist.