Devoirs Hebdomadaire N°13
CDL...DH13
M. Joseph DASSE BRIKA
  

        

Rappels : Factorielle n pour n entier >=0  est 
définie par n ! = 1 si n=0 et (n-1) ! * n sinon



On a écrit le programme du calcul de 
n! selon cette définition :   



  n!
  

    { n >= 0 } ; 
    
    
i := 0 ; f := 1 ;   

    
{ i = 0 & f=1 & n >= 0 } ;
    

    
while (i < n) do 
    

    
      i := i+1 ; 
    

    
      f := f * i   

    
end ; 

    
{ f = n !}   

  




On prend pour invariant { f = i ! & n >=i }



QUESTION 1 : montrez la correction totale de ce 
programme. 




Certains préfèrent "un i qui 
décroît"...  ils ont alors écrit un autre programme du calcul de n! 
:   



  n!
  

    { n >= 0 } ; 
    
    
i := n ; f := 1 ;   

    
{ i = n & f=1 & n >= 0 } ;
    

    
while (i >0) do   

    
      f := f * i ; 
    

    
      i := i-1 
    

    
end ; 

    
{ f = n !}   

  




Avec l'invariant { f * i ! = n! & i >=0 } 
  


Mais cela n'est pas satisfaisant car à la sortie 
de la boucle { f * i ! = n! & i >=0 & ~(i>0)} est une formule fausse !! 
  


Alors on modifie 
le prédicat de contrôle de la boucle (i >0) 
pour le prédicat de contrôle de la boucle (i>1)




  n!
  

    { n >= 0 } ; 
    
i := n ; f := 1 ;   

    
{ i = n & f=1 & n >= 0 } ; 

    
while (i >1) do   

    
      f := f * i ; 

    
      i := i-1   

    
end ; 

    
{ f = n !}   

  




QUESTION 2 : Donnez un invariant (inspiré 
fortement du précédent) et un variant pour la boucle et montrez la correction 
totale du programme. 




Utilisation de DJ-HOARE :   


    
  
  1. Dans un fichier, 
  fact.pl 
  par exemple, dans le même répertoire que DJ-HOARE.pl on 
  déclare l'opérateur factoriel (!) par 
  
    
  :- op(120 , xf , '!!').      ('!!' pour 
  éviter le conflit avec ! (cut) de Prolog) suivi du fait Prolog  
    
  hoare(<<séquent hoare correspondant au programme correct de la question 
  2>>).     
    2. 
  
  2. Lancer DJ-Hoare par un double clic sur 
  DJ-HOARE.pl puis 
  charger aussi fact.pl
   par 
  ?- [fact]. 
    3. 
  
  3. Lancer la validation du programme par
  ?- hoare(P) , P. 
    4. 



QUESTION 3 : Montrez le contenu de 
fact.pl 
et montrez les obligations de preuve et le 
programme bien documenté obtenus en répondant 
SYSTEMATIQUEMENT "3." 
(conjecture) à toutes les 
questions de DJ-HOARE. 





  

  

    

      
      Question 1:
    

    

       
      
      
{ n >= 0 } ; 
i := 0 ; f := 1 ; 
{ i = 0 & f=1 & n >= 0 } ; 
while (i < n) do 
      i := i+1 ; 
      f := f * i 
end ; 
{ f = n !} 

      
Le programme est il correct ?

      Prenons l'invariant I = { f = i! & n >=i }

      P = { i = 0 & f=1 & n >= 0 },   Q = { f = n !},   B = { i < n } 

      S = i := i+1 ; f := f * i 

      

      Il s'agit de valider la boucle while du programme.

      

      1-Prouvons P->I:

      

      { i = 0 & f=1 & n >= 0 } -> { f = i! & n >=i } 

      

      Car si i=0 et f=1 alors i!= 1 donc f=i!

      et comme n =0 alors on a bien n>=i.

      

      2-{B & I};S;{I}

      

      { i < n & f = i! & n >=i }

      

      {f*(i+1) =(i+1)! & n>=(i+1)}

       i := i+1 ;

      {f*i =i! & n>=i}

       f := f * i; 

      {f = i! & n >=i}

      

      Reste donc a prouver:

      { i < n & f = i! & n >=i } -> {f*(i+1) =(i+1)! & n>=(i+1)}

      

      On sait que (i+1)! = i! * (i+1), donc si f=i! alors (i+1)! = f * 
      (i+1)

      Et si n>i alors n>=(i+1)

      

      3-{I & ~B}->Q

      

      { f = i! & n >=i & n <= i } -> { f = n !} si n >=i & n<=i 
      alors n=i et comme f=i! alors f=n!

      

      Ces 3 premieres etapes ont permis de valider le corps de la boucle.

      On doit mainteant prouver que la boucle se termine.

      

      soit V le variant de boucle tel que V = n-i

      

      4-B->V > 0 { i < n } -> n-i > 0

      si i<n alors effectivement n-i >0.

      

      5-{B};A:=V;S;{V<A}:

      {i < n }

      

      { n-(i+1) < n-i }

       A:=n-i

      { n-i+1 < A }

       i := i+1 ;

       f := f * i;

      { n-i < A } 

      

      Reste a prouver:

      {i<n} -> { n-(i+1) < n-i }

      Effectivement n-(i+1) < n-i est toujours vrai si i<n.

      

      Le programme est correct.

    

    

      

    

    

      
      Question 2:
    

    

       
      
      
{ n >= 0 } ; 
i := n ; f := 1 ; 
{ i = n & f=1 & n >= 0 } ; 
while (i >1) do 
      f := f * i ; 
      i := i-1 
end ; 
{ f = n !} 

Programme Correct?
Invariant I = { f * i! = n! & i >=0 } 
Variant V = i 


1- { i = n & f=1 & n >= 0 } -> { f * i! = n! & i >=0 }:
-i=n et f=1 donc f * i! = n! => i!=n!
-si i=n et n>=0 alors i>=0.

2-{B & I};S;{I}
{i>1 & f*i!=n! & i>=0};S;{f*i!=n! & i>=0}

{i>1 & f*i!=n! & i>=0}

{ f*i*(i-1)! = n ! & (i-1)>=0 } 
 f := f * i ;
{f*(i-1)!=n! & (i-1)>=0}
 i := i-1 ;
{f*i!=n! & i>=0}

Pour prouver {i>1 & f*i!=n! & i>=0} -> { f*i*(i-1)! = n ! & (i-1)>=0 }
On sait que i*(i-1)! = i!, donc on a bien f * i*(i-1)! = f*i! = n!
Et comme i>1, i-1 sera bien >=0.

3-{I & ~B}->Q
{ f * i! = n! & i >=0 & ~(i>1)} -> { f = n !}

~(i>1) donne i<=1 et comme i>=0 donc i=1 ou 0
Ainsi i! = 1! = 0! = 1 => f * i! = n devient f=n!

4-B->V > 0 { i >1 } -> { i > 0 } est toujours vrai.

5-{B};A:=V;S;{V<A}:
{ i >1 } 

{i-1<i}  A:=i
{i-1<A}  f := f * i ;
 i := i-1 ;
{i<A}

{ i >1 } -> {i-1<i} 
i-1<i est toujours vrai lorsque i>1

Ce programme est donc correct.
(le corp de boucle est correct et la boucle se termine.)

      		
    

    

  



  
    		
  

  

      
      Question 3:
    

  

       
      
      Programme fact.pl:

        

          
          
:- op(120 , xf , '!!').

hoare([n>=0] '|-' i := n '.,' f:=1 '.,' 
while (i>1)     
invariant { f*(i'!!')=(n'!!') & i>=0}
variant {'i'}  
do (f:=f*i '.,' i:=i-1) end '.,'
{ f=n'!!'}).


          		
        

      

      		
    

  

       
      
      Obligations de preuves et programme bien documenté:

        

          
          
Obligation de preuve liée à une conjecture faite en : 11111121
 [n>=0, i>1&f*i'!!'=n'!!'&i>=0]'|-'f*i* (i-1)'!!'=n'!!'&i-1>=0 

Obligation de preuve liée à une conjecture faite en : 112121
 [n>=0, ~i>1, f*i'!!'=n'!!'&i>=0]'|-'f=n'!!' 

Obligation de preuve liée à une conjecture faite en : 14121
 [n>=0, i>1]'|-'i>0 

Obligation de preuve liée à une conjecture faite en : 111114121
 [n>=0, i>1]'|-'i>i-1 

Obligation de preuve liée à une conjecture faite en : 1111111
 [n>=0, true]'|-'1*n'!!'=n'!!' 


programme bien documenté : 
      {true}
   i:=n;
      {1*i!!=n!!&i>=0}
   f:=1;
      {f*i!!=n!!&i>=0}
      {i>1}
   a_1:=i;
      {a_1>i-1}
   f:=f*i;
      {a_1>i-1}
   i:=i-1;
      {a_1>i}
   while i>1
      invariant  {f*i!!=n!!&i>=0}
      variant  {i}
   do
         {i>1&f*i!!=n!!&i>=0}
      f:=f*i;
         {f* (i-1)!!=n!!&i-1>=0}
      i:=i-1;
         {f*i!!=n!!&i>=0}
   end;
      {~i>1&f*i!!=n!!&i>=0}
      {f=n!!}



          
 

        

      

      
      
 

    

  

    

    
  

  

    

            
FIN_dh13

  

  

    

    
  

  

    

            
ACCUEIL
            CONTACT
            FAVORIS ANNALES
            DH1
            DH2
            DH3 DH4 DH5 DH6
            DH7
            DH8
            DH9
            DH10 
            DH11 DH12 DH13 DH14 
            DH15 DH16