uv16472

Rappels : si dans un tableau sémantique aucune règle ne peut plus être appliquée à aucun noeud et que des branches ne sont pas fermées on dira que la démonstration est impossible.

Q1 : Quelles sont les démonstrations possibles et impossibles parmi :
(I) [ x ( C(x) & P(x) )] |- x C(x) & x P(x)
(II) [ x C(x) & x P(x)] |- x ( C(x) & P(x) )
(III) [ x C(x) & P(a)] |- x ( C(x) & P(a) )
(IV) [ x ( C(x) v P(x) )] |- x C(x) v x P(x)
(V) [ x C(x) v x P(x)] |- x ( C(x) v P(x) )

Informellement : à un moment donné la machine est dans un état (e0 , e1 ou e2), alors la lecture d'un 0 ou d'un 1 la fait passer dans un autre état selon le dessin et le caractère b ou a est émis. La machine est démarrée dans l'état e0.

Q2 : Construire le programme Prolog de la simulation correspondante.
Remarque : l'ENTREE et la SORTIE sont des listes. ENTREE une liste de 0 et de 1 (donnée) , SORTIE une liste de a et de b (attendue)...
Exemple : ?- simulMealy([1,0,1,1,1,1,0,0,1] , SORTIE).
SORTIE = [a,a,a,b,b,b,a,b,a]

i := 0;
while (i!=n & i<n) do
i := i+1;
V[i] := 0;
end;

Q3.1 : Donnez tous les éléments et toutes les assertions qui permettent d'établir la preuve de ce programme.

Q3.2 : A partir de Q3.1, construire la preuve de correction totale du programme

4-Java : on projette de simuler en Java le comportement de l'automate de la question 2 :

Rappel : L'automate est démarré dans l'état 'E0' et, par exemple : (les entrées étant données sur la ligne de commande)
>java TestAutomate 1 0 1 1 1 1 0 0 1
a a a b b b a b a

Une analyse objet selon de "pattern état" donne le diagramme de classes de la page suivante.

Rappels :
-> les flèches simples symbolisent une relation du type 'use'.
-> les flèches avec un triangle symbolisent la relation d'héritage.
-> devant les attributs ou les méthodes :
    . + symbolise public
    . - symbolise private
    . # symbolise protected
-> abstract désigne une classe ou une méthode abstraite

Code de la méthode 'Etat.sortie' :

public void sortie(char s) {
   System.out.println(s);
}

Q4 : Donner une implantation des classes java du schéma.