Ci-dessous, les différences entre deux révisions de la page.
Les deux révisions précédentes Révision précédente Prochaine révision | Révision précédente | ||
enseignement:logique:projet:2013 [2013/11/17 15:18] rthion [Mise à jour du projet] |
enseignement:logique:projet:2013 [2013/12/19 12:53] (Version actuelle) ecoquery [Organisation du projet] |
||
---|---|---|---|
Ligne 55: | Ligne 55: | ||
<note important> | <note important> | ||
Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. //Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles// | Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. //Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles// | ||
- | Le projet est à rendre après les vacances de Noël sous la forme d'une archive comme celle qui vous est fournie. //Les modalités exactes du rendu seront données en temps utile//. | ||
</ | </ | ||
Ligne 256: | Ligne 255: | ||
* '' | * '' | ||
- | La fonction | + | La fonction |
- | - mettre la valeur de '' | + | |
- | - s'il reste des variables à affecter, appeler | + | - sinon: |
- | - sinon tester la valeur de la cnf | + | |
- | * si la formule | + | - Appeler |
- | | + | - si l' |
- | | + | |
- | | + | - Appeler |
+ | | ||
+ | | ||
+ | |||
+ | |||
+ | <note warning> | ||
+ | * il n'y a pas besoin de faire de '' | ||
+ | * on peut déterminer que toute les variables ont été affectées en comparant '' | ||
+ | </ | ||
Modifier la fonction main de façon à: | Modifier la fonction main de façon à: | ||
Ligne 292: | Ligne 299: | ||
La première étape pour vérifier un additionneur n-bits consiste à générer sa spécification sous forme de formules. | La première étape pour vérifier un additionneur n-bits consiste à générer sa spécification sous forme de formules. | ||
- | On considère que les entrées sont données par les variables '' | + | On considère que les 2 * n entrées sont données par les variables '' |
- | On utilisera les formules suivantes: | + | On utilisera les formules suivantes |
* S = t ⇔(u ⇔ w) : cette formule est vraie si le chiffre des unités de la somme des valeurs de t,u et w est 1 (première formule de l' | * S = t ⇔(u ⇔ w) : cette formule est vraie si le chiffre des unités de la somme des valeurs de t,u et w est 1 (première formule de l' | ||
* R = (t ⇒ (u ∨ w)) ∧ (¬t ⇒ (u ∧ w)) : cette formule est vrai si la retenue de la somme des valeurs de t, u et w est 1 (deuxième formule de l' | * R = (t ⇒ (u ∨ w)) ∧ (¬t ⇒ (u ∧ w)) : cette formule est vrai si la retenue de la somme des valeurs de t, u et w est 1 (deuxième formule de l' | ||
- | La génération de cette spécification par récurrence peut être définie comme suit: | + | La génération de cette spécification par récurrence |
- | * Additionneur 1-bit: | + | * Additionneur 1-bit : on retourne le vecteur V=[B,A1] de taille //2// avec |
- | * A1 = S [ p1/t, q1 / u, ⊥ / w] | + | * A1 = S [ p1/t, q1 / u, ⊥ / w], on calcule cette formule en construisant la substitution |
- | * B1 = R [ p1/t, q1 / u, ⊥ / w] | + | * B = R [ p1/t, q1 / u, ⊥ / w], idem que précédemment, |
- | * Additionneur // | + | * Additionneur //n//-bits : soit V' |
- | * A//n// = S [ p//n// / t, q//n// / u, B//n-1// / w ] | + | * A//1// à A//n-1// : on ne change rien : A'// |
- | * B//n// = R [ p//n// / t, q//n// / u, B//n-1// / w ] | + | * A//n// = S [ p//n// / t, q//n// / u, B' / w ], B' est le dernier bit de sortie d'un additionneur à //n-1//-bit que l'on va l' |
+ | * B = R [ p//n// / t, q//n// / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à //n-1//-bits, c'est le bit de poids le plus fort du vecteur V', c'est la retenue de l' | ||
- | Écrire la fonction '' | ||
- | On pourra procéder de manière itérative en s'appuyant sur deux '' | + | === Exercices === |
- | A la fin de la fonction, il suffira de renvoyer les '' | + | |
+ | * Écrire la fonction | ||
+ | * Écrire les tests unitaires associé et vérifier | ||
+ | * Modifier ensuite le '' | ||
- | Modifier ensuite le '' | + | <note tip>Vous disposez de la fonction |
- | <note tip>En testant votre programme, même avec des additionneurs très petits, vous verrez que le temps de calcul est élevé. La partie suivante vise à améliorer cette situation.</ | + | <note tip>En testant votre programme, même avec des additionneurs très petits, vous verrez que le temps de calcul est élevé. La partie suivante vise à améliorer cette situation. La partie suivante est indépendante de la présente, le deux peuvent donc être travaillées en parallèle.</ |
===== Quatrième partie: optimisations ===== | ===== Quatrième partie: optimisations ===== | ||
Ligne 401: | Ligne 411: | ||
* v3, 16/10/13: informations compilation Windows/ | * v3, 16/10/13: informations compilation Windows/ | ||
* v4, 16/11/13: aide sur erreur '' | * v4, 16/11/13: aide sur erreur '' | ||
+ | * v5, 24/11/13: modif partie sur additionneur | ||
+ | * v6, 18/12/13: mise à jour de la description de la fonction '' |