Test sur l'Atelier B

- Vous disposez du corrigé du test (adressé par courriel
 et mis sur le
blog spec1, AVANT le ds spec1)
- Je vous ai fourni le barème mais celui-ci ne
m'a pas été redonné. Je
n'ai pas reçu votre auto-notation (je l'avais
demandé AVANT le Ds de
spec1. Cela aurait évité ....)
- Ne me souvenant pas de ce barème, de toutes
 façons non utilisé par vous,
j'ai pris le barème suivant :
Question 1 : sur 2
Question 2 : sur 3. Si vous avez spécifié une
 opération qui ne fait rien,
vous avez prouvé qu'elle respecte l'invariant !
 La note est 0.
Question 3 : sur 3
Question Spécifications de contraintes :
3 points par contrainte
Question 4 : sur 6
Si vous n'avez pas pris en compte les deux
 contraintes (certains ont
changé le sujet pour pouvoir prouver !
espérons qu'en entreprise vous ne
changerez pas la demande du client !)
 et que vous avez fait une opération
prouvée et qui enregistre un rattrapage : 2 points.

Bien sûr, j'ai vérifié que pour chaque question :
- vous n'avez pas mis une précondition fausse.
I & P => [Op] I
est vérifié quand I ou P sont faux ! (voir
la table de vérité de =>)
- vous n'avez pas mis une contradiction dans l'invariant
- vous avez bien une opération qui fait une modification :
ceux qui ont écrit quelque chose comme
PRE x : ENS &
x : trucc
THEN
trucc := trucc \/ [x}
END;
ont eu une obligation de preuve triviale !
mais leur opération est inutile !

Tout ce que je viens d'écrire fait l'objet
d'un chapitre du poly. Et j'ai
insisté en TD et en cours.

- les notes seront affichées demain matin.