Ce que j'ai fait en cours ce matin (8h 45 9h 45)

• Un test de mathématiques. les questions et les réponses sont sur le présent bloc-notes sauf pour la dernière question que voici (pour les absents)

Sachant que A est un ensemble d'éléments atomiques (un SET !) , soit le prédicat (écrit en ASCII, mais pour le test c'était écrit en notation mathématique)

d : A --> A & d : A * A

Ce prédicat est bien typé OUI NON
Justification de votre réponse.

Réponse :
NON
si d est un élément d'un produit cartésien, c'est donc un couple (à ne pas confondre avec un ensemble singleton, dont l'élément est un couple). d ne peut pas alors être aussi une fonction totale.

Cette question était là pour vérifier une cohérence entre les réponses aux questions 1 et 2 et cette question.

• Le théorème du séquencement
• Le théorème de la boucle, INVARIANT de boucle, VARIANT de boucle. Un exemple illustratif
• Et comme à chaque cours, quelques compléments :

• Les ASSERTIONS
• La substitution "devient tel que"

Comme toujours j'insiste sur le pourquoi (ce que vous ne notez surtout pas !!! , Dommage : "il n'y a de vent favorable que pour celui qui sait où il veut aller")
Pourquoi donc les ASSERTIONS en B ?

Voici un exemple :

On vous a dit qu'un étudiant est membre au plus d'un groupe.
Qu'un groupe a au plus un étudiant qui le représente.
Et que tout étudiant représentant un groupe est membre du groupe qu'il représente.
(exemple plusieurs fois repris dans mes cours)

Vous avez spécifié :
aPourGroupe : ETUDIANT +-> GROUPE &
aPourReprésentant : GROUPE +-> ETUDIANT &
aPourReprésentant~ <: aPourGroupe

Par un raisonnement rigoureux (mais non formel) vous en déduisez que :
Un groupe a au plus un étudiant qui le représente.

Reste à le prouver avant de revoir votre interlocuteur et lui dire :
"D'après ce que vous m'avez dit j'en ai déduit que "Un groupe a au plus un étudiant qui le représente."

La clause ASSERTIONS est faite pour cela !

ASSERTIONS
aPourReprésentant ~ : ETUDIANT +-> GROUPE

L'Atelier B doit prouver les assertions.

Remarquons qu'on peut alors écrire :
aPourGroupe : ETUDIANT >+-> GROUPE &

Les assertions servent aussi à aider l'Atelier B. Vous pouvez ainsi prouver de petits lemmes dont il pourra se servir dans la preuve. C'est la preuve interactive.