***une idée... ***
de ce qui était attendu
en première session 2001
***uv16472***


1-preuves :


retour énoncé


2-Prolog :

etud(18/12/75,zazou,[],jean,h01234).
etud(19/11/65,charles,[],pol,h12034).
etud(8/2/74,boule,balle,julie,h74125).
etud(4/5/81,dean,[],james,h19681).
etud(5/10/68,monroe,[],marilyn,h11112).
etud(1/1/75,gin,[],mary,h22222).

dh(h22222,[dh(8,2),dh(1,2),dh(9,2),dh(3,1),dh(2,2),dh(4,3),dh(5,3),dh(7,2),dh(6,3)]).
dh(h19681,[dh(9,3),dh(3,2),dh(2,1),dh(4,3),dh(5,2),dh(7,2),dh(6,1)]).
dh(h11112,[dh(8,1),dh(1,2),dh(9,1),dh(3,2),dh(2,1),dh(4,2),dh(5,3),dh(7,2)]).
dh(h74125,[dh(6,3),dh(8,2),dh(9,1),dh(3,3),dh(2,2),dh(4,1)]).
dh(h12034,[dh(8,2),dh(2,3),dh(3,1),dh(4,3),dh(5,3),dh(7,3),dh(6,3)]).

bonus(CODE,NOM,PRENOM,BONUS) :-
etud(_,NOM,_,PRENOM,CODE), dh(CODE,LDH),
nbDH23(LDH,NB), ptBonus(NB,BONUS).
bonus(NOM,PRENOM,BONUS) :-
etud(_,NOM,_,PRENOM,CODE), dh(CODE,LDH),
nbDH23(LDH,NB), ptBonus(NB,BONUS).

ptBonus(7,2).
ptBonus(8,3).
ptBonus(9,3).
ptBonus(6,1).
ptBonus(5,1).
ptBonus(NB,0) :- member(NB,[0,1,2,3,4]).

nbDH23([dh(_,2)|LDH] , NB) :- nbDH23(LDH , N), NB is N+1.
nbDH23([dh(_,3)|LDH] , NB) :- nbDH23(LDH , N), NB is N+1.
nbDH23([dh(_,1)|LDH] , NB) :- nbDH23(LDH , NB).
nbDH23([],0).

retour énoncé


3-Hoare :

INV1 = ( " x (x ³ 1 Ù x £ i) -> t1[x]=t2[x] Ù i £ k-1 )
VAR1 = k-i+1
POST CONDITION 1 = ( " x (x ³ 1 Ù x £ k-1) -> t1[x]=t2[x] )
INV2 = ( " x (x ³ 1 Ù x £ k-1) -> t1[x]=t2[x] ) Ù
( " x (x ³ k Ù x < i) -> t1[x+1]=t2[x] Ù k £ i Ù i£ n )
VAR2 = n-i+1
Correction totale de :
{t1[1..n] Ù t2[1..n-1] Ù n > 0 Ù 1£ k Ù k£ n} ;
i:=1;
while (i¹ k-1)
invariant : { INV1}
variant : { VAR1 }
do
i := i+1;
t2[i] := t1[i] ;
end;
{ " x (x³ 1 Ù x£ k-1) -> t1[x]=t2[x] }
3.1 – (t1[1..n] Ù t2[1..n-1] Ù n > 0 Ù 1£ k Ù k£ n Ù i=0) -> INV1 Vraie par défaut
3.2 – en remontant :
{ " x (x ³ 1 Ù x £ i-1) -> t1[x]=t2[x] Ù i £ k-1Ù i¹ k-1}
; trivial
{ " x (x ³ 1 Ù x £ i) -> t1[x]=t2[x] Ù i+1 £ k-1};
i := i+1;
{ " x (x ³ 1 Ù x £ i-1) -> t1[x]=t2[x] Ù i £ k-1};
{ " x (x ³ 1 Ù x £ i-1) -> t1[x]=t2[x] Ù i £ k-1 Ù t1[i]=t1[i] };
t2[i] := t1[i] ;
{ " x (x ³ 1 Ù x £ i-1) -> t1[x]=t2[x] Ù i £ k-1 Ù t1[i]=t2[i] };
{ " x (x ³ 1 Ù x £ i) -> t1[x]=t2[x] Ù i £ k -1}

3.3– en remontant :
(" x (x ³ 1 Ù x £ i-1) -> t1[x]=t2[x] Ù i £ k-1Ù i = k-1) ->
" x (x ³ 1 Ù x £ k-1) -> t1[x]=t2[x] : trivial

4– Arrêt : (t1[1..n] Ù t2[1..n-1] Ù n > 0 Ù 1£ k Ù k£ n Ù i=1) -> k-i+1 > 0 : trivial
5– en remontant :
{k-i<k-i+1} : toujours vraie
AR1 := k-i+1;
{k-i<AR1}
i:=i+1;
{k-i+1<AR1}

retour énoncé


4-Java :


import java.util.*;
import java.io.*;
public class Client{
   public static void main(String[] args){
      Service service=Service.getService();
      try{ System.out.println(service.requete(args[0]));
      }catch(Exception e){
           System.out.println(e.getMessage());
      }
   }
}

class ProxyServeur extends Service {
   private Serveur serveur= new Serveur();
   static private Service service=new ProxyServeur();
   private ProxyServeur(){}
   static public Service getService(){
      return service;
   }
   public String requete(String identite)throws Exception{
      if(autorisation.getProperty(identite).equals("autorisé")){
        return serveur.requete(identite);
      }else{throw new Exception("accès refusé");}
   }
}