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}
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é");}
}
}