***une idée... ***
de ce qui était attendu
en juin 2000
***uv16472***
1-preuves :
2-Prolog :
simulMealy(ENTREES , SORTIES) :-
simulMealy(e0 , ENTREES , SORTIES).
simulMealy(EtatCourant ,[E|ENTREE] , [S|SORTIE]) :-
traite(EtatCourant , E , S , EtatSuivant),
simulMealy(EtatSuivant ,ENTREE , SORTIE).
simulMealy(_ ,[ ] , [ ]).
traite(Etat1 , E , S , Etat2) :-
transition(Etat1 , E , S , Etat2).
transition(e0 ,0 , a , e1).
transition(e0 ,1 , a , e2).
transition(e1 ,0 , b , e1).
transition(e1 ,1 , a , e2).
transition(e2 ,0 , a , e1).
transition(e2 ,1 , b , e2).
3-Hoare :
{V[1..n] & n>0}
i := 0;
{V[1..n] & i=0 & n>0}
while (i!=n &i<n)
invariant
{[universal]x (1<=x & x<=i) -> V[x]=0}
variant {n-i}
do
i := i+1;
V[i] := 0;
end;
{[universal]x (1<=x & x<=n) -> V[x]=0}
4-Java :
/* TestAutomate.java */
public class TestAutomate extends Object {
public Automate automate = new Automate();
public void simulMealy(String args[]) {
for(int i=0;i<args.length;i++){
automate.traite(Integer.parseInt(args[i]));
}
}
public static void main (String args[]) {
new TestAutomate(). simulMealy(args);
}
}
/* Automate.java */
public class Automate extends Object {
public Etat e =new E0();
public Automate() {}
public void traite(int entree) {
e= e.transition(entree);
}
}
/* Etat.java */
public abstract class Etat extends Object {
public abstract Etat transition(int entree);
public void sortie(char s) {
System.out.println(s);
}
}
/* E0.java */
public class E0 extends Etat {
public E0() {}
public Etat transition(int entree) {
sortie('a');
switch(entree){
case 0: return new E1();
case 1: return new E2();
default : throw new Error();
}
}
}
/* E1.java */
public class E1 extends Etat {
public E1() {}
public Etat transition(int entree) {
switch(entree){
case 0: sortie('b');return this;
case 1: sortie('a');return new E2();
default : throw new Error();
}
}
}
/* E2.java */
public class E2 extends Etat {
public E2() {}
public Etat transition(int entree) {
switch(entree){
case 0: sortie('a');return new E1();
case 1: sortie('b');return this;
default : throw new Error();
}
}
}
