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/24 21:51] rthion [Formules de spécification] |
enseignement:logique:projet:2013 [2013/12/19 12:53] 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 299: | Ligne 306: | ||
La génération de cette spécification par récurrence pour //n//-bits peut être définie comme suit: | La génération de cette spécification par récurrence pour //n//-bits peut être définie comme suit: | ||
- | * 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 |
- | * B = 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' / w ], où | + | * A//1// à A//n-1// : on ne change rien : A'// |
- | * B = R [ p//n// / t, q//n// / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à // | + | * 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 à // | ||
Ligne 312: | Ligne 320: | ||
* Écrire les tests unitaires associé et vérifier | * É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. La partie suivante est indépendante de la présente, le deux peuvent donc être travaillées en parallèle.</ | <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.</ | ||
Ligne 402: | Ligne 412: | ||
* v4, 16/11/13: aide sur erreur '' | * v4, 16/11/13: aide sur erreur '' | ||
* v5, 24/11/13: modif partie sur additionneur | * v5, 24/11/13: modif partie sur additionneur | ||
+ | * v6, 18/12/13: mise à jour de la description de la fonction '' |