une idée 2 --- 2002

1- Q1 :

      cpv(X , Y) :- h(X) , d(Y).
      cpv(X , Y) :- p(X) , r(Y).
      cpv(X , Y) :- cpv(X , Z) , cpv(Z , Y).
      
      h(bob).
      
      p(rex).
      
      r(jeannot).
      
      d(X) :- p(X).

Q2 : du fait de la récursivité gauche dans cpv(X , Y) :- cpv(X , Z) , cpv(Z , Y).

Q3 : {h(bob) , h(rex), h(jeannot) ,
p(bob) , p(rex), p(jeannot) ,
r(bob) , r(rex), r(jeannot) ,
d(bob) , d(rex), d(jeannot) ,
cpv(bob , bob) , cpv(bob , rex) , cpv(bob , jeannot) ,
cpv(rex , bob) , cpv(rex , rex) , cpv(rex , jeannot) ,
cpv(jeannot , bob) , cpv(jeannot , rex) , cpv(jeannot , jeannot) }

Q4 : Tp(@) = {h(bob) , p(rex), r(jeannot)}
Tp(Tp(@)) = Tp(@) U {cpv(rex , jeannot) , d(rex)}
Tp(Tp(Tp(@))) = Tp(Tp(@)) U {cpv(bob , rex)}
Tp(Tp(Tp(Tp(@))) = Tp(Tp(Tp(@))) U {cpv(bob , jeannot)}
Tp(Tp(Tp(Tp(@))) = Tp(Tp(Tp(Tp(@)))) = SEM chaînage Avant = {cpv(rex , jeannot) , d(rex) , cpv(bob , rex) , cpv(bob , jeannot)}

Donc la réponse à la question cpv(bob , jeannot) ? est OUI!!!

2- Prolog /DATALOG :

2.1

dh('I12345' , 5 , 1).
dh('I12345' , 6 , 2).
...

cpt(N) :- retract('CPT'(N)), ! ,
          NN is N+1,
          assert('CPT'(NN)).
cpt(0) :- assert('CPT'(1)).

selectCountFromDH(_) :-
   dh(_,_,_),
   cpt(_),
   fail.
selectCountFromDH(Count) :- 'CPT'(Count).

2.2

selectFromDHWhere(CHAMPS=VALEUR) :-
      table(DH),
      arg(Num , DH , CHAMPS),
      dh(M,Dh,Note),
      arg(Num, dh(M,Dh,Note), VALEUR),
      write(dh(M,Dh,Note)),nl,
      fail.
selectFromDHWhere(_) :- write(ouf),nl,nl,nl.

3-1 Sémantique Structurelle

3-1 :- op(111,xfx, # ).
normeQ(A # 1 , A):- integer(A) , !. 
normeQ(A # B , AA) :- pgdc(A,B,P), 1 is B / P , ! , AA is A / P.
normeQ(A # B , AA # BB) :- pgdc(A,B,P), BB is B / P , AA is A / P.
fraction(A # B , A # B). fraction(A , A # 1) :- integer(A).

3-2 Sémantique Structurelle
evaq(A  #  B,VQ)  :- normeQ(A # B , VQ).
evaq(Q1 + Q2,VQ) :- fraction(Q1,A # B) , fraction(Q2,C # D),
   Num is A*D + B*C,Dem is B*D, normeQ(Num # Dem , VQ).
evaq(Q1 * Q2,VQ) :- fraction(Q1,A # B) , fraction(Q2,C # D),
   Num is A*C, Dem is B*D, normeQ(Num # Dem , VQ).
evaq(Q1 / Q2,VQ) :- fraction(Q1,A # B) , fraction(Q2,C # D),
   Num is A*D, Dem is B*C, normeQ(Num # Dem , VQ).

   ?-evaq((456 # 101 + 33 # 2 )*(18 # 47 + 24# 7 )/( 1# 181 )).   
	P = 481752315#33229 
	Yes

3-2 DCG

exq(VQ) --> tq(VQ1) , ['+'] , exq(VQ2) , {evaq(VQ1  +  VQ2 , VQ)}.
exq(VQ) --> tq(VQ).

tq(VQ)  --> fq(VQ1) , ['*'] , tq(VQ2) , {evaq(VQ1  *  VQ2 , VQ)}.
tq(VQ)  --> fq(VQ1) , ['/'] , tq(VQ2) , {evaq(VQ1  /  VQ2 , VQ)}.
tq(VQ)  --> fq(VQ).

fq(VQ)  --> [X1] , [ # ] , [X2] , {integer(X1) , integer(X2) , evaq(X1  #  X2 , VQ)}.
fq(X)  --> [X] , {integer(X)}.
fq(VQ)  --> ['('] , exq(VQ), [')'].

om --> ['*'].
om --> ['/'].
/*
?- exq(Q , ['(',456, # ,101 , '+' , 33, # ,2 , ')' , '*' , '(' , 18, # ,47 , '+' , 24, # ,7 , ')' , '/' ,  '(' , 1, # ,181 , ')'] , []).

Q = 481752315#33229 ;

No
*/

4- Java :

abstract class AutomateDeMoore{
  public Etat etatCourant;
   //@ invariant etatCourant != null;

   public AutomateDeMoore(){  //@ assume etatCourant != null;
        }

   //@ requires entree>=0 & entree<etatCourant.etatsSuivants.length;
   //@ modifies etatCourant;
   //@ ensures \result==etatCourant;
   //@ ensures etatCourant==\old(etatCourant).etatsSuivants[entree];
   public Etat transiter(int entree){ 
     etatCourant=etatCourant.transiter(entree);
     return etatCourant; 
   }
   // la sortie est associée à l'état courant (Moore)
   //@ modifies etatCourant.sortie;
   //@ ensures \result==etatCourant.sortie;
   public char action(){
           return etatCourant.action();
   }
}

//public
class Automate extends AutomateDeMoore{

   Etat e0,e1,e2;
   //@ invariant \typeof(etatCourant)==\type(E0) || \typeof(etatCourant)==\type(E1) || \typeof(etatCourant)==\type(E2);
   //@ invariant etatCourant==e0 || etatCourant==e1 || etatCourant==e2 ;
   //@ invariant \typeof(e0)==\type(E0) & \typeof(e1)==\type(E1) & \typeof(e2)==\type(E2) ;
   //@ invariant e0.etatsSuivants[0] == e1 & e0.etatsSuivants[1] == e2;
   //@ invariant e1.etatsSuivants[0] == e1 & e1.etatsSuivants[1] == e2;
   //@ invariant e2.etatsSuivants[0] == e1 & e2.etatsSuivants[1] == e2;
   //@ invariant Etat.infEntree==0 & Etat.maxEntree==1;
   //@ invariant (\forall Etat e; e.etatsSuivants.length==2 );
   
   // modifies e0.singleton,e1.singleton,e2.singleton;
   //@ modifies Etat.infEntree,Etat.maxEntree;
   // ensures e0.singleton & e1.singleton
   // ensures \fresh(e0) & \fresh(e1) & \fresh(e2) & \fresh(etatCourant);
   //@ ensures etatCourant==e0;
   public Automate(){
         
         //créer les états et les connecter par des transitions ordonnées
         etatCourant=e0=new E0();
         e1=new E1();
         e2=new E2();
         e0.setEtatsSuivants(new Etat[]{e1,e2});
         e1.setEtatsSuivants(new Etat[]{e1,e2});
         e2.setEtatsSuivants(new Etat[]{e1,e2});
     // set e0.singleton=true;
     // set e1.singleton=true;
            //@ set Etat.infEntree = 0 ;
            //@ set Etat.maxEntree = 1;
   }     
   
     //@ also_ensures \old(etatCourant) == e0 && entree == 0 ==> etatCourant == e1
     //@ also_ensures \old(etatCourant) == e0 && entree == 1 ==> etatCourant == e2; 
     //@ also_ensures \old(etatCourant) == e1 && entree == 0 ==> etatCourant == e1;
     //@ also_ensures \old(etatCourant) == e1 && entree == 1 ==> etatCourant == e2;
     //@ also_ensures \old(etatCourant) == e2 && entree == 0 ==> etatCourant == e1;
     //@ also_ensures \old(etatCourant) == e2 && entree == 1 ==> etatCourant == e2;
    public Etat transiter(int entree){
             return super.transiter(entree);
     }

   //@ invariant e0.sortie=='a' & e1.sortie=='b' & e2.sortie=='c';

}



// public      
abstract class Etat{
          
   //@ ghost static public int infEntree;
   //@ ghost static public int maxEntree;

   protected /*@ spec_public non_null*/ Etat[] etatsSuivants;
  //@ invariant \nonnullelements(etatsSuivants) && etatsSuivants.length>0;
  
  public Etat(){
     //@ assume \nonnullelements(etatsSuivants)&& etatsSuivants.length>0;

          }
          
  //@ requires \nonnullelements(etatsSuivants) && etatsSuivants.length>0;
  //@ modifies this.etatsSuivants;
  //@ ensures this.etatsSuivants==etatsSuivants;
  public void setEtatsSuivants(Etat[] etatsSuivants){
          this.etatsSuivants=etatsSuivants;
          }
          
  //@ ensures \result==etatsSuivants;        
  public Etat[] getEtatsSuivants(){
          return etatsSuivants;
          }
          
  //@ requires i>=0  & i<etatsSuivants.length;
  //@ ensures \result==etatsSuivants[i]; 
  public Etat getEtatsSuivants(int i){
          return etatsSuivants[i];
          }

  //Automate de Moore : l'action de sortie est associée à l'état
  protected char sortie;
  
  //@ modifies sortie;
  //@ ensures \result==sortie;
   abstract public char action();
  
  //@ requires entree>=0 & entree<etatsSuivants.length;
  //@ ensures \result != null 
  //@ ensures \result==this.etatsSuivants[entree];
  public Etat transiter(int entree){
          return etatsSuivants[entree];
          }
}

          
//public 
final class E0 extends Etat{
   
   //@ ensures sortie=='a';
   public E0(){
           sortie='a';
           }
           
   public char action(){ 
           return sortie;
   }

}

//public
final class E1 extends Etat{
        
   //@ ensures sortie=='b';
   public E1(){
           sortie='b';
           }
              
   public char action(){ 
           return sortie;
   }
}

//public
final class E2 extends Etat{
   //@ ensures sortie=='c';
   public E2(){
           sortie='c';
           }
              
   public char action(){ 
           return sortie;
   }
}


public class EtatEntierSimple{
    static Automate detecteur;
  // ensures detecteur.etatCourant == detecteur.e2; 
  public static void main(String[] args){
          detecteur= new Automate();
          detecteur.transiter(0);
          detecteur.action();
          detecteur.transiter(1);
          detecteur.action();
          detecteur.transiter(1);
          detecteur.action();
  }
}