Spec 1 (Spécifications 1) Software Specifications

Gaston Bachelard

2010-01-20T10:19:00.000+01:00

Gaston Bachelard
(1884-1962)
A lire :
"La formation de l'esprit scientifique", Librairie philosophique J. Vrin, 1938, 1972
" La psychanalyse du feu", Idées, Gallimard

- " Qui est enseigné doit enseigner. Une instruction qu'on reçoit sans la transmettre forme des esprits sans dynamique, sans auto-critique. Dans les disciplines scientifiques surtout, une telle instruction fige en dogmatisme une connaissance qui devrait être une impulsion pour une démarche inventive. Et surtout, elle manque à donner l'expérience psychologique de l'erreur humaine. (...) Comme seule utilité défendable des "compositions" scolaires, j'imagine... Le premier de la classe reçoit comme récompense, la joie de donner des répétitions au second, le second au troisième et ainsi de suite jusqu'au point où les erreurs deviennent vraiment trop massives. "
- " Un concept est devenu scientifique dans la proportion où il est devenu technique, où il est accompagné d'une technique de réalisation. On sent donc bien que le problème de la pensée scientifique moderne est, de nouveau, un problème philosophique intermédiaire. Comme aux temps d'Abélard, nous voudrions nous fixer nous-même dans une position moyenne, entre les réalistes et le nominalistes, entre les positivistes et les formalistes, entre les partisans des faits et les partisans des signes. C'est donc de tous côtés que nous offrons à la critique. " p. 61
- " Une culture bloquée sur un temps scolaire est la négation même de la culture scientifique. Il n'y a de science que par une Ecole permanente. C'est cette école que la science doit fonder. Alors les intérêts sociaux seront définitivement inversés : la Société sera faite pour l'Ecole et non pas l'Ecole pour la Société" p. 252
- "Pour un esprit scientifique, toute connaissance est une réponse à une question"
Ceux qui vous vendent des bases de connaissances, se trompent sur ce qu'est une connaissance !
- " Rien ne va de soi. Rien n'est donné*. Tout est construit."
- " Toute désignation d'un phénomène connu par un nom savant apporte une satisfaction à une pensée paresseuse. "

La deuxième conférence sur Teaching B

2009-02-12T14:53:00.001+01:00

aura lieu le 8 juin 2009 à la Cité des Congrès de Nantes
http://teachingbconference.blogspot.com/

Conscience et Mécanisme

2008-11-27T13:41:00.000+01:00

http://iridia.ulb.ac.be/~marchal/bxlthesis/consciencemecanisme.html

Thèse Bruno Marchal, 1994

Un site pour les b a ba sur les ensembles et relations

2008-11-27T13:23:00.000+01:00

ICI

TThe Long, Dismal History of Software Project Failure

2008-10-02T08:16:00.001+02:00

http://www.codinghorror.com/blog/archives/000588.html

TThe Long, Dismal History of Software Project Failure

2008-10-02T08:16:00.000+02:00

http://www.codinghorror.com/blog/archives/000588.html

Retraite ...mais ça continue !

2008-06-21T10:56:00.000+02:00

L'auteur de ce bloc-notes part en retraite...mais continuera à alimenter ce bloc-notes.

Aléa jacta est (dé, datum, donnée, information)

2008-04-03T09:03:00.002+02:00

Alea, en latin, signifie "dé" ou "jeu de dés", par extension désignait le sort, le hasard, etc.
Le latin tardif lui a préféré datum, "ce qui est donné". (Orlando de Rudder, Aperto libro, Larousse, ISBN : 2-03-330023-4)

Une donnée est une information. En probabilité, on parle d'événements (aléatoires). Si avant de tirer une boule de l'urne, on sait qu'elle sera noire, ce n'est pas un événement, ce n'est pas une donnée, ce n'est pas une information. L'information, c'est ce qui réduit l'incertitude (voir aussi le concept de "bien économique"). Voir les "scoops". Si je conserve la donnée, c'est que, pour moi, à la mémoire faiblarde, ce que j'ai inscrit dans le fichier, est une information (voila d'ailleurs pourquoi je vais la chercher). Le jour où mon nom sera pour moi une info ce ne sera pas bon signe pour mon entourage !

L'axiome du choix

2008-02-13T17:43:00.002+01:00

Dans le polycopié vous avez la présentation des axiomes de la théorie des ensembles et ceux retenus par B.
Parmi les axiomes, il y a l'axiome du choix.
Il dit que si on dispose d'un ensemble d'ensembles non vides et disjoints deux à deux, par exemple l'ensemble des groupes de première année (je rappelle qu'un étudiant ne peut être membre de plus d'un groupe), alors on peut constituer un ensemble en prenant un élément dans chacun des ensembles.
Ca paraît étonnant de devoir avoir un tel axiome.
On trouvait étonnant aussi de devoir avoir l'axiome des parallèles ...
On en a eu besoin quand on s'est rendu compte qu'avec les autres axiomes, on ne pouvait prouver qu'on pouvait bien constituer ...
Alors on a proposé l'axiome du choix. C'est Ernst Zermelo qui l'a introduit en 1904.
Paul Cohen a prouvé en 1963 qu'il est impossible de déduire l'axiome du choix des autres axiomes.

Teaching the B method, the blog

2008-02-06T18:34:00.000+01:00

The B method : from research to teaching,
Conference,
Nantes,
France

Cité Internationale des Congrès
June 16, 2008

Blog here :

http://teachingbconference.blogspot.com/

Une application de B

2008-02-05T20:19:00.000+01:00

Des pages d'information sur le système KVS de la SNCF, pour ceux qui aiment les trains.
Une des premières application de la méthode B.

20 ans déjà

2008-02-03T16:36:00.000+01:00

En rangeant mes papiers (il faut bien partir en retraite), et en remplissant ma poubelle, je retrouve une lettre de la direction des systèmes de signalisation de GEC Alsthom datée d'octobre 91.

Extraits :

"GEC Alsthom a commencé à utiliser la méthode B en 1987, pour respécifier, en vue de certification, le système SACEM installé sur la ligne A du RER à Paris, et en service depuis septembre 1988. Ce système a permis d'accroître le débit de la ligne, l'intervalle entre trains étant réduit de 2 min 30 à 2 min, en améliorant la sécurité.

Nous l'utilisons actuellement pour la réalisation du logiciel de contrôle de vitesse appelé KVS, destiné à la SNCF. (...)"

Filocours, riboulware et croquargent

2008-01-31T14:38:00.000+01:00

c'est le titre d'un article de 01 Informatique, reproduit dans un papier de Gilbert Cristini qui fut rédacteur en chef de O1 Informatique.

Le sous-titre est :"Afin d'écarter les Pieds Nickelés de la formation, l'Education Nationale ne pourrait-elle promouvoir un label pour les cours d'informatique ?"

C'était en sept 1969, l'année chantée par Serge Gainsbourg.

Qui aujourd'hui poserait une telle question ? C'était l'ancien temps. Aujourd'hui, tout le monde sait ce qu'est l'informatique. Il suffit de naître avec un ordinateur dans la salle d'accouchement !

Les fonctions partielles et les 'valeurs nulles"

2008-01-31T14:20:00.000+01:00

Message reçu ce jour :
" Re bonjour,

Concernant les commandes de billets transports chez CARLSON, quelques petites informations complémentaires utiles.Lorsque vous allez rechercher le contrat cadre, il faut être vigilant car plusieurs lignes vous sont proposées.
Pour l'achat des billets ferroviaires, vous avez 2 lignes :1ère ligne :2006FCS9996036/1 - Fourniture de titres de transports - LOT 1 - 4600000035 - 0010 - 60.01 (grpe marchandises) correspond à l'achat de billets de transport avec la dérivation budgétaire 62561. Sans TVA.

2ème ligne :2006FCS9996036/1 - Fourniture de titres de transports - LOT 1 - 4600000035 - 0020 - 60.07 (grpe marchandises) correspond à la prestation de service (frais d'agence) avec la dérivation budgétaire 6228. Avec TVA non déductible de 19,6%

Il faut donc créer 2 lignes au moment de l'établissement de votre commande, l'une pour les billets, l'autre pour les frais d'agence.

Ceci est incontournable.

Même procédure pour les billets d'avion (national ou international).

Nous sommes à votre disposition pour vous guider."

Eh oui, vous devez savoir cela. J'ai traité plusieurs fois de la normalisation des schémas relationnels. La bonne théorie évite bien des commentaires.

Attendons le prochain message sur :
-les livres
-les ...

et le
"ceci est incontournable".

C'est comme la semi-décidabilité bien connue de vous tous (voir vos copies)

Débloquer l'économie français qu'il dit Attali !

La vraie vie, SIFAC, le Ministre, et le génie logiciel

2008-01-30T10:24:00.000+01:00

" SIFAC évolue tous les jours.En effet, jusqu'à hier lundi nous pouvions "autoriser" et "calculer" l'OM. Cela ne bloquait aucunement la possibilité de pouvoir modifier à souhait l'OM en fonction de la réalité du déplacement.OR, et toute mise à jour n'est PAS BONNE, car depuis aujourd'hui mardi, losque nous calculons l'OM, cela a pour effet de transmettre en comptabilité générale (donc à l'agence comptable). Autre effet, c'est que cela nous INTERDIT toute modification ultérieure ; cela veut dire que lors du retour de l'agent, nous ne pouvons modifier son déplacement en fonction de la réalité de celui-ci.Vous imaginez bien les problèmes que cela va entraîner pour le remboursement.Le problème est soulevé auprès du concepteur afin de débloquer la situation.DONC, EN ATTENDANT, NE PAS CLIQUER SUR "CALCULER". Cela n'empêchera pas la visualisation et l'impression de l'OM (enfin normalement...)."

OM : Ordre de Mission
Rappel : l'Administration paye des services effectués.
Mais là il faudrait que les informaticiens aient suivi notre enseignement à l'IUT en I.O.S. (droit, etc.)
Ce matin , à notre cours de 8 heures : 8 absents sur 25 inscrits.
Un message reçu ce jour
Bof , bof , bof !

A quoi bon spécifier les logiciels ! A quoi bon enseigner les spécifications. Comme l'a demandé notre ministre de l'Enseignement Postérieur, il faut que les étudiants notent les enseignants du supérieur. Cette mesure doit faire partie des propositions du rapport Attali pour l'amélioration de la productivité de l'économie française. Oui, oui ... *

Donc les étudiants qui sont informaticiens depuis leur plus tendre enfance se foutent bien de la spécification et des demandes de ces imbéciles d'utilisateurs qui ne savent pas utiliser leurs logiciels.

Bof, bof ...
tant que ce ne sont pas les mêmes qui font les logiciels embarqués sur l'Airbus, le TGV, le métro !

Je rappelle que ce que nous enseignons à l'IUT est utilisé, a été utilisé pour Meteor, le métro de Calcutta, de New-York, pour la navette de Roissy, etc.

* sur France Culture nous avons appris ce matin que maintenant les élèves traduits en Conseil de discipline pouvaient se faire assister d'avocats. Que les parents attaquaient le lycée si les notes de leurs enfants n'étaient pas bonnes.
Je vois le proviseur chapitrant ses enseignants : faites moi de bonnes notes sinon je vous fais payer les frais de tribunal ...

Qu'en disent les clercs ?

"La démission des clercs ?"

Notes du test sur l'Atelier B

2008-01-28T15:59:00.000+01:00

du groupe 3 sont affichées sur la porte de mon bureau depuis ce matin 9h 30.

Les notes du "DS" sont affichées

2008-01-28T11:04:00.000+01:00

Merci aux étudiants des 4 groupes qui m'ont adressé leur auto-notation.
Les notes affichées sont résultat de ma propre évaluation.

Il est vivement conseillé, afin que le contrôle serve à quelque chose, que vous
compreniez vos erreurs ou que vous étudiez ce que vous n'avez pas appris.

En particulier la numération par position !

Il est clair que quand on lit dans une copie de maths en fin de semestre (ouf ! je ne suis pas seul à lire des ...) :
"la somme infinie des entiers positifs est égale à zéro" ....

Les matheux n'ont rien compris ! On peut te piquer sur ce qui est sur ton compte épargne + ce qui est sur ton compte chèque +... et la somme fera zéro .... sur tes comptes !

tu vois les étudiants ont raison ! Il faut bien mettre des bonnes notes. Un peu de psycho voyons !

La numération indienne

2008-01-27T16:15:00.000+01:00

Complément au corrigé de la dernière question du "DS"*.

"A partir du IIIe siècle, les Indiens avaient donné un nom à chaque puissance de dix jusqu'à 10 puissance 17, de sorte que pour eux, le nombre
523622198443682439
est (en traduisant les chiffres en français et en écrivant, comme les Indiens, les unités en tête, puis les dizaines, etc.) :
neuf et trois dasha et
quatre shata et
deux sahasra et
huit ayuta et
six laksha et
trois prayuta et
quatre vyarbuda et
huit padma et
deux shankha et
six samundra et
trois madhya et
deux antya et
cinq parardha.
Cette notation sanscrite suggère de ne faire apparaître que les chiffres (sans mentionner les termes dasha, shata, etc. ), ce qui conduit à la notation décimale de position"

Celle que nous utilisons depuis qu'elle nous est parvenue via les Arabes et l'Andalousie. Si le vocabulaire est de cardinal 10 on parle de base 10, si il est de cardinal 2, on parle de base 2 et de "numération binaire".

J-P Delahaye
Les inattendus mathématiques, Belin, p. 21

* Il faudrait changer ce nom ! ça fait plusieurs années que les DS n'en sont plus. Appelons-les "contrôles de connaissances (?!) , de compréhension (?!) individuelles faits en amphi"

Test sur l'Atelier B

2008-01-27T08:30:00.000+01:00

- 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.

Une perle naturelle ....

2008-01-25T16:47:00.000+01:00

Toutes les questions du contrôle se terminaient par " ... sur 1" ou "...sur 5" selon le poids de la question dans la note finale.

A la 9ième question "Qu'est-ce que la semi-décidabilité ?", j'ai eu cette réponse :

"La semi-décidabilité sur 1 est une décidabilité sur 1 presque achevée. La décidabilité sur 1 étant automatique la semi-décidabilité est donc semi-automatique."

J'ai eu peur ! Je m'attendais à "la semi-décidabilité sur 1 est 1/2"

Je suis vache, j'ai mis 0/1 à la réponse. Un bon prof aurait dit "je ne vais pas descendre au 1/2 point ! la notation ce n'est pas comme faire de la mesure en menuiserie !, je mets 0,5. Quel prof sûr de lui qui se permet de descendre au 1/2 point ! "

0, 5 sur 1 , c'est 5/10, 10/20.

Facile ! on fait ainsi pour toutes les questions où on a obtenu un texte. Et tout le monde a au moins 10.

On est les meilleurs !

J'ai vu faire cela. On m'a dit : c'est quand même mieux que de mettre des notes sans avoir lu les copies ! Ben dame !

Comme me disait mon père : "si tu cherches ceux qui font plus mal que toi, tu seras toujours satisfait !"

Quelques lectures conseillées

2008-01-24T08:33:00.000+01:00

Quelques lectures conseillées :

Merci à Laurent Bloch


Notes sur le langage, la culture et la société
(sans oublier la
fonction publique française) :

http://laurent.bloch.1.free.fr/spip.php?article108

Contre les méthodes de conduite de projet :

http://www.laurentbloch.org/spip.php?article137

Nature du travail informatique :

http://www.laurentbloch.org/spip.php?article138

Voici des questions du prochain examen de spec

2008-01-23T21:27:00.000+01:00

" Sur un bateau, il y a 12 moutons et 13 chèvres, quel est l'âge du capitaine ?"
"Dans une classe, il y a 7 rangées de 4 tables, quel est l'âge de la maîtresse ?" *
Bon, pour celle-là je donne la réponse de bien des élèves.
"Facile, 7 * 4 = 28, la maîtressse elle a 28 ans"

Bien plus facile que le paradoxe de Bertrand Russell !

Trop facile !

Alors ce sera :

Epiménide le Crétois dit que tous les Crétois sont menteurs.

Alors Epiménide : Menteurs ?
ou
Epiménide /: Menteurs ?

Lisez :
Stella Baruk, C'est à dire en mathématiques ou ailleurs,
"Pour une arithmétique de la liberté ...", Seuil, 1993

et
Stella Baruk, L'âge du capitaine. De l'erreur en mathématiques, Seuil, 1985

C'est Stella Baruk qui a introduit le terme automaths.

Et revoyez Mais où est passé l'euro ? (Les clients, le groom et l'hôtelier) sur ce bloc-notes. Vous faites de "la compta-gestion", avez-vous compris ce qu'est la "comptabilité en parties doubles" ? Vérifiez avec notre spec. Ce sera aussi une occasion d'introduire à notre cours de spec2 sur la communication entre processus.

Avec un faible effort on peut éviter...

2008-01-23T20:41:00.001+01:00

de se faire repérer ...

il fait partie et non il fait parti
le parti politique de Dudule
dépendance fonctionnelle et non dépendence fonctionel (surtout quand je vous l'ai écrit correctement sur la feuille de réponse !)

j'ai fourni et non j'ai fournit

et on n'écrit pas en Français :

" car il se raseré lui-même"

Si vous ne faites pas de spécifications formelles, il faudra apprendre la syntaxe du Français !

Décidabilité et semi-décidabilité

2008-01-23T20:21:00.000+01:00

J'ai insisté sur ce point. J'ai rappelé ce qui était arrivé à d'anciens étudiants qui avaient envoyé un message sur le forum B en rouspétant parce que l'Atelier, quand ils écrivaient une conjecture fausse, ne leur dise pas que la conjecture était fausse : des correspondants leur ont écrit qu'ils feraient bien d'étudier leur cours !

Et je vous ai dit de vous méfier. Si en stage on vous demande de réaliser certains programmes dont on a prouvé que le problème est indécidable, c'est que soit que le demandeur n'a pas appris ses cours (et alors là, c'est dommage que les stages ne soient pas rémunérés, car il apprendrait le coût de la "non connaissance") ou ... ou qu'il veut tester votre niveau.

Et lire le polycop ou les messages du bloc-notes ou d'utiliser wikipedia ou de consulter les cours de bonnes universités ou ...

Bof ! il suffit de raconter ce qui passe par la tête ! par exemple :
"La semi-décidabilité est ce qui permet de mettre en forme le début de l'Atelier B"
C'est quoi le début de l'Atelier B ? et on peut savoir ce que peut être cette mise en forme ?

ou encore
"La semi- décidabilité c'est la moitié d'une décimale"

ou encore
"C'est le fait d'avoir une décision à prendre face à plusieurs choix possibles, que la machine ne peut faire elle-même, d'où l'obligation de faire des implantations."

ou encore
"... c'est quand l'Atelier B ne veu (sic) pas prouver car c'est "c'est bon mais pas suffisant" (comme condition, précondition, invariant) "
L'Atelier qui veut ! "c'est bon mais pas suffisant"

ou encore
"C'est donc lorsqu'on peut choisir qu'à moitier (sic) "

Un étudiant qui ne sait pas répondre, donne une leçon à l'enseignant :
Je demandais d'expliquer bien et court ce qu'est la semi-décidabilité. Il m'écrit :

"bien et court" peut-être assimilé au terme "conscit". Merci !

Oh Oh !

2008-01-23T18:25:00.000+01:00

s inclus dans A
S <: A
se récrit :
s appartient à P * P
s : POW * POW

P étant le P de Powerset

C'est nouveau, ça vient de sortir

Et aussi :

s inclus dans A,
s <: A
se récrit :
s appartient à A.
s : A

Et encore :

s inclus dans A,
s <: A
se récrit :
{s} appartient à A
{s} : A

Et encore :

1 < x+1 < 10 donc
0 < x < 9 donc
x : 0..9
que je viens de lire plusieurs fois.

Et encore :
Une fonction partielle de A vers A est égale au produit cartésien de l'ensemble des sous-ensembles de A par l'ensemble des sous-ensembles de A.

Facile les maths et l'informatique !
Et heureusement que nous avons le bac, premier examen universitaire (oui, oui ! D'ailleurs le jury est présidé par un enseignant de l'enseignement postérieur (pardon, supérieur).

Produit cartésien ...

2008-01-23T17:56:00.000+01:00

carthésien,
j'ai déjà trouvé quartésien

... et pourquoi pas quarthésien!

Descartes, celui du poële ..., celui du Prythanée militaire de la Flèche (Pays de la Loire)

Attention à la lecture ...

2008-01-23T17:37:00.000+01:00

Un étudiant du groupe 3 a écrit, explicitant son calcul de la plus faible précondition

[x := x + 1] (x : 1..10)

Je rappelle que cela se lit :
la substitution de x + 1 à x établit l'invariant (x appartient à l'ensemble 0..10).
(Et non que x = l'ensemble des entiers de 0 à 10 !!!!)

Voici ce qu'a écrit l'étudiant :

[x := x + 1] (x : 1..9)

alors que la plus faible précondition est x : 1..9
Quand on fait en effet la substitution dans x : 1..10, ça donne :
x+1 : 1..10
ce qui donne (petites classes)
x : 1..9

Tant que x appartient à l'ensemble de 1 à 9 on peut ajouter + 1 à x.
C'est écrit plusieurs fois sur mes pages web et j'ai fait cette manip plusieurs fois en cours
et TD. Et même en couleur !

Ce qu'il a écrit est la plus faible précondition ...
x + 1 : 1..9
ce qui donne :
x : 1..8

Mais on lui a mis la note maxi. C'est qu'on veut être bien noté !
Et on justifie par "il n'a pas fait attention. Mais comme nous sommes télépathe, nous savons que c'est une coquille".

Je vous rappelle le premier vol d'Ariane V et le "dépassement de capacité".
Je vous rappelle aussi tous ces services de distribution d'eau qui, plus le client consommait, plus ils versaient de l'argent au client. ...
car ils ne prenaient pas en compte les changements de compteur. Et comme la consommation est calculé ainsi
Conso = nouvel index du compteur - ancien index du compteur
quand on mettait un nouveau compteur à un index inférieur à l'ancien index de l'ancien compteur, vous qui faites de la compta, vous savez que ...

Et je vous rappelle la dernière question du DS... vous voyez le rapport ?

J'ai eu comme réponse à la question :

voici le résultat du calcul de la précondition :
x : 1..9 & x < 9
ce qui se lit :
x doit appartenir à l'ensemble des entiers de 1 à 9
et x doit être inférieur à 9

Là je n'ai pas mis 1/1 à la réponse !

Est-il encore temps ?

2008-01-23T17:28:00.000+01:00

A tous ceux qui m'ont écrit que je ne pouvais écrire :
cardinal de Truc parce que Truc n'était pas un ensemble mais une relation,

J'ai aussi trouvé:

domaine de {1, 2, 3} !

je demande ce qu'ils ont fait pendant les TD d'Atelier B, ce qu'ils ont fait pendant les TD de spec, ce qu'ils ont fait pendant les TD de maths. Je ne parle pas des cours ...

Merci de me répondre. La formation des enseignants est permanente. Et comme je veux être bien noté par ces étudiants pour améliorer l'économie française (application d'une des mesures du rapport Attali ...)

Constat

2008-01-23T16:26:00.000+01:00

Un très grand nombre d'étudiants, au bout de plusieurs mois en département informatique d'IUT, NE savent pas comment lire un entier écrit dans une base donnée selon la numération par position
(niveau CM1),

Alors que cela leur a été enseigné par au moins deux enseignants et que la question avait été présentée en amphi et qu'un chapitre du poly traitait la question etc.
ne savent pas ce qu'est une fonction, confondent un prédicat avec une substitution, une expression avec un prédicat, etc.

Le comble est le fait que j'avais posé en test, corrigé, insisté sur les premières questions qui nécessitaient de savoir la différence entre appartenance et inclusion, entre l'ensemble A et le produit cartésien A * A et de savoir ce qu'est une fonction.

Alors savoir ce qu'est un invariant, une précondition !

Conclusion : ce sont les profs qui sont mauvais. Sinon ils auraient de bonnes notes. CQFD*
Et ils n'ont pas adapté leur matière au public. Qu'ils fassent comme les Restau U qui ont mis des fontaines à coca et de la bouffe rapide pour satisfaire leur public. "Education Nationale" vous dis-je !

Je vois déjà ce que donnera la boxologie avec de tels "informaticiens"

* Mais rappel : on sort des DPLG (Diplômés Par Le Gouvernement) mais faut pas exagérer, SGDG (Sans Garantie du Gouvernement).

Merci au groupe 4 pour son auto-notation du DS

2008-01-23T13:29:00.001+01:00

Il me reste à noter de mon côté...
J'espère trouver les mêmes notes.

J'aimerais aussi avoir votre auto-évaluation de votre dossier de TD
en prenant en compte les consignes écrites dans le dossier des
sujets de TD.

Encore une autre question

2008-01-23T13:20:00.000+01:00

Bonjour,
Pour la question 6.4 Le raffinage,
J'ai mis dans l'invariant:
size(profseq) <= maxprof & ran(profseq) = prof (comme vu en TD de spec1
avec M.HadjRabia)
alors qu'a la correction il est mis seulement ran(profseq) = prof
Ai-je quand même bon ?

Vous aviez le corrigé dans mon polycop page 189. J'y implante un ensemble de portes sur une suite injective. Et la preuve a été faite.

A voir

Ayant parcouru quelques copies ... j'ai mis un corrigé où il n'y a que la partie reliant la variable abstraite à la concrète ... pour avoir des points en plus. MAIS vous avez raison

"Marking scheme", Règles de notation du DS

2008-01-23T07:59:00.000+01:00

Comme mes collègues britanniques, je fournis un schéma de notation pour le DS.
Vous disposez du barème de chaque question.

Je détaille :
1.1.1
un point par bonne réponse
1.1.2
bien typé : 0, 5
justification correcte : 1,5
1.2
0,5 par bonne réponse (je ne demandais pas de préciser "prédicat, expression ou substitution" quand c'était mal typé)
moins 1 par mauvaise réponse
Note mini à 1.2 sera 0
1.3
1 si bon, 0 sinon
1.4
1 si bon, 0 sinon
1.5
Un point par question bien répondue
Zéro sinon
Pour la réponse, "Aucune, voici la bonne réponse", veuillez
me communiquer votre réponse si elle est différente de
celle que j'ai fournie. Il y a, en effet, pas mal de réponses
possibles, ne serait-ce que parce que l'on peut utiliser le
langage prédicatif au lieu du langage ensembliste.
2.1
1 si réponse claire. 0 sinon.
2.2
3 si bonne réponse. Si vous n'avez pas mis :
& et : ETUDIANT
& coll : COLLEGE
compter bon (si le reste est bien mis !)
6.4
Complément à l'invariant sur 2, 0 si incomplet ou erroné
Remarque : j'accepte qu'on n'ait pas mis la contrainte sur
la taille de la suite. MAIS bien sûr en aucun cas celui qui
a fourni une réponse comme vous la trouverez dans mon
poly page 189 ont parfaitement bien répondu !
initialisation sur 1
3.1.1
0 si clé incomplète
3.2
un par bonne réponse
moins un par mauvaise réponse
note mini égale à zéro
4
première question sur 1
deuxième question sur 2
0 si réponse fausses. Mais si delta de 1 pour la réponse à 1,
compter 0,5

Note finale à donner sur 20.

Encore une question d'un étudiant.

2008-01-22T21:58:00.000+01:00

Je n'en ai pas reçu pendant l'enseignement.
Elles arrivent maintenant. Il n'est jamais
trop tard dans l'enseignement.
=================================

Pouvez-vous me dire si la question suivante
(Q11 du QCM) peut accepter
cette réponse :
=> Réponse 6; Aucun voici la bonne
réponse : prof =
(etudQuiEstTitulaireDe~;situationAnterieure~)
[{maitrise}]
On donne {maitrise} à etudQuiEstTitulaireDe~
qui nous renvois un ensemble
inclu dans etud. Puis situationAnterieure~
reçoit ce sous ensemble
d'étudiant qui lui même renvois un ensemble
 de professeur concerné qui se
trouve finallement égal à l'ensemble des profs,
 puis que les profs sont
d'anciens étudiants titulaires de la maitrise.

=======
Réponse :
1) Attention à l'orthographe même sur un
 courriel. Mais je sais, on y fait
facilement des coquilles.
envoyer. Je renvoie
finalement
inclus, incluse
2)
etudQuiEstTitulaireDe~: TYPEDEDIPLOME <-> etud &
situationAnterieure~ : etud <-> prof
Donc
etudQuiEstTitulaireDe~;situationAnterieure~)
[{maitrise}]
est bien typé.
Et donne l'ensemble des profs, lesquels sont
 d'anciens étudiants titulaires
de la maîtrise. Ca répond bien à la définition
 informelle.
Mais je dois reconnaître que "au mieux"
est ambigü. On peut faire mieux que le <: 
de ma réponse 5. En remplaçant le <: par =.
C'est la réponse 3.
Donc d'accord pour votre réponse. Votre
spec me semble plus facile à comprendre.
J'avais pensé écrire "qui sont le plus proches
de l'énoncé". Mais il aurait fallu définir
une fonction de proximité !
Contrairement à ce que l'on pense souvent, un QCM
intelligent n'est pas facile à faire.
Mais j'ai abandonné les sujets demandant une
spec car année après année,j'avais des copies
de textes respectant de moins en moins une syntaxe
formelle.
Dommage...

La nouvelle immatriculation des véhicules

2008-01-22T21:31:00.000+01:00

Avant :

AEteImmatriculéPar : véhicules * (Date * Date) >+> IMMATRICULAION

/* Un véhicule est immatriculé de telle date à telle date par un et un seul n° d'immatriculation,
lequel n'immatricule qu'un seul véhicule
Mais au cours de sa vie, il peut avoir plusieurs immatriculations */

Maintenant :

AEteImmatriculéPar : véhicules >-> IMMATRICULATION

Exercice :
Spécifier les opérations changementDImmatriculation dans l'ancien système (par exemple quand le véhicule a son propriétaire qui change de département de domicile).
Rechercher la ou les circulaires ministérielles qui précisent si dans le nouveau système, quand un véhicule sera détruit, son immatriculation pourra être réutilisée... et spécifier en conséquence.

C'est bien l'auto-notation

2008-01-22T19:40:00.000+01:00

... enfin un contrôle utile. Et un corrigé lu et discuté. C'est tellement rare. Merci à ceux qui en profitent.

Voici un dernier message :

> Bonsoir,
> Je viens de regarder la seconde version de votre corrigé et il y a
> quelques éléments à la question 2.2 que je trouve "étrange". Vous avez
> marqué :
>
> coll:COLLEGE
>
> Or si on marque cela, "coll" n'appartient pas forcément à "college", sauf
> que pour ajouter un nouveau couple à notre fonction partielle, il aurait
> fallut que coll:college.

Je n'ai pas mis cela ? J'ai mis à jour à 7 heures ce matin... j'ai donc fait une c... (d'ailleurs voir le blog)

IL FAUT que coll : college sinon on pourrait mettre dans le co-domaine un college qui n'est pas dans college.

Et est-ce que c'est nécessaire de mettre
> et:ETUDIANT & coll:COLLEGE si on affirme que et:etud et coll:college vu
> qu'on a affirmer dans l'invariant que etud<:ETUDIANT & college<:COLLEGE.

===============
Rappel du cours :

En B on ne fait pas d'inférence de type comme on le fait par exemple dans des langages fonctionnels ou comme on le faisait en BASIC où on ne typait pas explicitement les variables.

Quand on écrivait
5 + A l'interpréteur lisant un entier, puis le + , interprétait le + comme l'addition arithmétique et alors interprétait le A comme un entier. Inférence de type.
Si on écrivait
"toto" + A, le + était interprété comme une concaténation et A comme de type chaîne de caractères.
On dit "polymorphisme de l'opérateur +"

En B on type explicitement. Ce que vous faites c'est de l'inférence de type.
En fait, il se peut que l'Atelier B en fasse parfois. Mais je préfère systématiquement typer. Ainsi si je me plante dans mon typage, l'atelier me le dira.

Le corrigé du DS de 2008

2008-01-21T17:36:00.001+01:00

Vous le trouverez ici. (avec correction de la correction. x : 0.. n , j'ai confondu avec le nombre d'entiers que l'on peut implanter sur le boulier (il faut faire -1 au chiffre fourni))
La feuille de réponse, vous la trouverez ici.

Le sujet sans typo, vous le trouverez ici.
... demain

Et ce message d'un étudiant ... et ma réponse :

 Bonjour,
>
> Pour la question 10 (1.5.10), vous indiquez
comme réponse la numero 4 soit
> : prof <: profQuiEstT itulaireDe~[{maitrise}]. Néemmoins, lors du DS,
> j'ai répondu 3 : prof = profQuiEstTitulaireDe
~[{maitrise}], et elle me
> semble aussi valide. En effet
profQuiEstT itulaireDe : prof -->
> TYPEdeDIPLOME. Or tout les profs
sont titulaires d'une maitrise. donc
> "prof = profQuiEstT itulaireDe~
[{maitrise}]" ou "prof <: profQuiEstT
> itulaireDe~[{maitrise}]" (car ce
n'est pas une inclusion stricte).
> Ais-je tors ? Si oui, ou se situe mon erreur ?

=================
J'ai mis comme réponse celle qui
correspondait au mieux à l'énoncé en
langage naturel. Certes 4 et l'extrait
d'invariant que vous considérez =>
3.
Vous n'avez pas d'erreur. C'est juste
une question d'interprétation de la
question. Donc 1/1 pour vous !
C'est bien les specs formelles !
P.S. : à moins que ce soit une co(q)uille,
attention : tors veut dire
tordu, avoir tord ...
J'ai, ai-je ...
Néanmoins (vient de néant moins)
=================
>
> Autre question, dans le corrigé,
pour le boulier vous dites que Mon Entier
> : 0..n avec n=1296. Or le chiffre
le plus grand est 5555 en base 6
> soit 1296 en base 10 (il se trouve
que j'ai mis 1410 dans le DS à cause
> d'une faute de frappe sur calculatrice
: j'ai écrit 5*5*6+5*6^2+5*6^3 au
> lieu de 5+5*6+5*6^2+5*6^3, mais le
bon résultat est 1295). Donc n=1296 ou
> n=1295 ?
>
Oh ! une calculatrice pour ça. Le crayon
et le papier évite les fautes de frappe.

Vous avez raison. Quand
j'ai rédigé le corrigé j'ai effectivement
eu dans la tête le nombre
d'entiers et non le n de x : 0 .. n.
J'ai changé le sujet par rapport à la
question posée en amphi et je n'ai pas
fait attention.
Attention ! si je vous réponds
bool(n=1296 or n=1295) = TRUE ...
La réponse bonne est n= 1295,
soit avec le 0, 1296 nombres. 1296
étant écrit ici en base dix.
========================
J'ai écrit ce matin note/20 au tableau,
20 étant écrit en base dix !

> Dernière question. Le barème du devoir
est sur 35. Desirez vous récupérer
> les note sur 35 ou preferez vous que
nous la ramenions sur 20 ?
>
> Je vous remercie
================
C'est moi qui vous remercie pour votre
courriel. D'autant plus que je
n'ai pas imprimé le corrigé (et donc
relu sur papier) que je vous ai
adressé ...


Et ce message d'un autre étudiant (je ne
fournis pas les noms car il s'est agi de
courriels "privés") :

1.2
=> Vous dites si c'est un prédicat,
une expression ou une substitution
dans les cas où les 'formules' sont mal
formées or vous avez dit de ne
faire que les bien formées.
====================
Vous avez raison. J'ai mis les * car certains
étudiants (mon expérience des années passées)
ne font pas la différence entre = et :=.
Mais pour vos réponses, vous deviez respecter
le sujet.
=======================
=> bool(card(var1) = card(var2)) vous dites
que c'est un prédicat, mais je
pense que c'est une expression car bool()
transforme un prédicat en
expression.
=====================
Oh ! je n'aurais pas dû regarder/écouter Arte
en tapant le corrigé !
Bien sûr, vous avez raison, j'ai loupé le bool !
Ca n'a pas de sens que de vouloir prouver
TRUE, que de vouloir prouver FALSE.
TRUE, FALSE sont des expressions (ou termes)
=====================
1.5.8
=> Vous donnez la réponse 1 comme bonne :
ensembledesetudiantsdelanationormandie ==
nationDOrigine~[{normandie}]
Or ran(nationDOrigine~) n'est pas un
ensemble d'étudiant !
J'ai répondu la question 5 personellement
car la composition fonctionne,
on met bien [{normandie}] et que
ran(nationDOrigine~;origineEtudiant~))
<: ETUDIANT =================
Oh ! c'est une erreur de frappe. Vous avez raison.
 Bien sûr j'ai rédigé la réponse 5 pas par hasard !
==================
2.2 => Vous donnez comme plus faible précondition :

et : ETUDIANT & et /: dom(aPourCollege) &
coll : COLLEGE & et : Coll

Je vois quelques erreurs, premièrement :
et : Coll (un étudiant appartient
à un ensemble Coll qui n'est même pas
un ensemble.

et : ETUDIANT n'est pas assez fort comme
précondition car
dom(aPourCollege) <: etud et non pas dans ETUDIANT.
 coll : COLLEGE, même remarque ran(aPourCollege)
 <: college et non pas dans COLLEGE.
J'ai donc mis : et : etud & coll :
college &  et /: dom(aPourCollege)
======================
Oh ! encore une faute de frappe.
C'est bien votre réponse que j'ai
 sur "mon corrigé" papier. La question était
 toute simple. Pour respecter la foncion,
 il fallait s'assurer que et /: dom(aPourCollege)
 et comme l'ensemble source était etud,
 il fallait que et : etud et comme l'ensemble
 cible était college, il fallait que coll :
 college. En effet, il ne fallait pas modifier
 ce qui était après le THEN. En fait, j'ai
donné une opération minimale.

===========================
Au sujet de la question 7.2
Plusieurs étudiants m'ont demandé pendant le
DS. "Où est définie r5 ?"
Pour utiliser la notation B, je devais nommer
la partie gauche de : (s1 * s2) +-> s2,
je l'ai nommé r5. Je vous donnais ainsi la
réponse à la question 7.1.1 ! Je ne pouvais quand
même pas mettre r1 à la place de r5 !
Le typage de r5 est respecté par la relation
r1.
 ========================
P.S. 1 Si vous m'adressez un courriel
 avec un texte mathématique, utilisez
 la notation ASCII de B. J'ai dû
interpréter le message car mon correspondant
 a utilisé une notation inconnue pour
les symboles mathématiques.
P.S. 2 Si
un collègue enseignant veut
 les sources Latex de ce sujet,
 qu'il me les demande.

The B Method: from Research to Teaching

2008-01-20T11:54:00.000+01:00

The B Method: from Research to Teaching
16 June 2008
Nantes
France

Call for Papers

In 2008 the University of Nantes will be holding
an extensive series of no less than 22 one-day
 conferences in a wide range of subjects from science
 and technology, biology and health, and human
 and social sciences. These will all take
place at the impressive large modern purpose-built
venue of the "Cite International
des Congress" in the centre of Nantes,
and are expected to attract up to
1250 participants altogether. Within such
a context the above one-day conference on the
B Method will be held on 16 June 2008.

Topics of interest will include
(but will not be restricted to):

* Tool support for software engineering with the B method,

* Teaching environments for the B method,

* The B method in the software engineering
curriculum,

* Combining the B method with other approaches,

* Case studies and exercises featuring
the B method,

* Use of the B method in disciplines other
than software engineering,

* New advances in the B method and their
incorporation into the
teaching curriculum.

SUBMISSION DATE
3 April 2008

NOTIFICATION DATE
1 May 2008

Program Committee
-----------------
Henri Habrias, Universite de Nantes, France [chair]
Rueda Camilo, Universidad Javeriana-Cali,
 Cali, Colombia
Steve Dunne, University of Teesside, UK
Michael Leuschel, Heinrich-Heine-Universität
 Düsseldorf, Germany
Mike Poppleton, University of Southampton, UK
Dominique Mery, Loria, Nancy, France
Ken Robinson, University of New South
Wales, Australia
Emil Sekerinski, McMaster University,
Canada
Elena Troubitsyna, Åbo Akademi University,
 Finland
Mark Utting, University of Waïkato,
 New Zealand
Guy Vidal-Naquet, Supelec, Gif-sur Yvette,
 France
Istenes Zoltán, Budapest, Hungaria



LOCAL ORGANIZATION
Christian Attiogbé, Pascal André,
Gilles Ardourel, Henri Habrias

It is expected that revised copies of
accepted papers will be published in
Electronic Notes in Theoretical Computer Science
(ENTCS), Elsevier Science
<http://www.entcs.org>.

Merci Arte

2008-01-20T10:24:00.001+01:00

Ce qui est bien à la maison, le dimanche matin, c'est que, quand je fais un travail peu gratifiant * (ce matin saisir en latex le corrigé du DS de demain) , je peux écouter la télé (difficile de la regarder, et encore je peux taper sans regarder mes doigts - merci au prof qui quand j'étais étudiant nous a conseillé d'apprendre à dactylographier - ).
Ce matin, Fadela Amara puis l'émission littéraire, puis maintenant Michel Serres (je vous en ai parlé quand j'ai traité du concept de modèle, en citant son exemple de la fable de La Fontaine, Le loup et l'agneau, repris dans mon polycop).
Dimanche dernier, c'était Albert Jacquard
Dimanche prochain, Jacqueline de Romilly que nous avons écoutée il y a deux ans lors de sa conférence à Audencia.

Merci Arte.

Le samedi matin, France Culture
dimanche matin, Arte

Si vous n'avez rien retenu de ce qui est dans ce bloc-notes, retenez au moins ce que je viens d'écrire !

Merci aux enseignants qui m'ont permis de jouir de ces émissions.

* j'espère qu'il y aura au moins un étudiant qui s'en servira. Ecolo, je n'en ferai pas un tirage papier en 100 exemplaires ! au moins j'aurai contribué à la santé de mes étudiants.

"la plus âpre des leçons"

2008-01-20T10:20:00.000+01:00

"Il continue à enseigner (...) aussi parce que c'est une leçon d'humilité, cela lui fait comprendre la place qui est la sienne dans le monde. Ce qu'il y a là d'ironique ne lui échappe pas : c'est celui qui enseigne qui apprend la plus âpre des leçons, alors que ceux qui sont là pour apprendre quelque chose n'apprennent rien du tout."

Goetze, Prix Nobel de littérature

Si vous avez loupé les cours et les td

2008-01-19T08:36:00.000+01:00

Vous pouvez toujours lire mes livres :

Henri Habrias, Le modèle relationnel binaire, méthode I.A. (NIAM), Paris, Eyrolles, 1988, ISBN : 2-12-08169

Henri Habrias, Introduction à la spécification, préface de Hervé Gallaire, présentation par Michael Jackson, Masson, 1993, ISBN : 2-225-82768-0

Henri Habrias, La mesure du logiciel, 2ième édition, corrigée et augmentée, Teknea, 1994, ISBN : 2-87717-045-4

David Lightfoot, La spécification formelle avec Z, traduit par H. Habrias, Teknea, 1994, ISBN : 2-87717-038-1

Henri Habrias, Dictionnaire encyclopédique du génie logiciel, Préface de Jean-Pierre Finance, Masson, 1997, ISBN : 2-225-85328-2

Henri Habrias, Les paradigmes des méthodes d’analyse et de conception in Génie logiciel: principes, méthodes et techniques A. Strohmeier, D. Buchs (Publié sous la direction de), 1996,Presses Polytechniques et universitaires romandes, ISBN:2-88074-296-X

Henri Habrias, Bibliographie commentée d’introduction aux spécifications formelles in Applications des techniques formelles au logiciel, ARAGO N° 20, Observatoire Français des Techniques Avancées, OFTA, Editions Tec & Doc, 1997, ISBN : 2-9060-2806-1

Henri Habrias, Lexique de l’objet et des composants logiciels in Architecture de logiciels et réutilisation de composants, ARAGO N° 24, Observatoire Français des Techniques Avancées, OFTA, Editions Tec & Doc, 2000, ISBN : 2-906028-10-X

M. Frappier, H. Habrias - Software Specification Methods, An Overview Using a Case Study, FACIT, Springer, 2000, ISBN : 1-85233-353-7
Site web associé, livre épuisé.

Une critique de ce livre.
Ils l'utilisent : lien1, lien 2, lien 3

Henri Habrias, Spécification formelle avec B, Lavoisier-Hermes, 2001, ISBN : 2-7462-0302-2

Henri Habrias, Petit dictionnaire à l'usage des lecteurs novices d'Abélard, Univ. de Nantes, 2001, ISBN : 2-906082-30-9

Jean Jolivet, Henri Habrias, Pierre Abélard à l'aube des universités, Unv. de Nantes, 2001, ISBN : 2-906082-31-7

Jean Jolivet, Henri Habrias (sous le direction de), Pierre Abélard, Colloque international de Nantes, PUR, ISBN : 2-86847-777-1, 2003

Henri Habrias, Marc Frappier, Software Specification Methods, Edition 2004, ISTE, U.K., USA, ISBN : 1-905209-34-7
nouveaux participants : E. Börger (ASM), L. Lamport (TLA), D. Cansell, D. Méry (Event B), et une classification des méthodes et un dictionnaire des termes utilisés.

et le polycopié en ligne

Henri Habrias, Spécifications avec B, IUT de Nantes, départ. informatique, 2007

"C'est peut-être vrai en théorie, mais en pratique c'est faux."

2008-01-18T19:16:00.000+01:00

L'art d'avoir toujours raison

Un petit livre de Schopenhauer, dans la collection Mille et Une Nuits, 2000 (100 pages, je sais que 100 pages même format 10 x 15 cm ça peut faire peur à un étudiant "nouvelle génération" (coco, "de nouvelle génération" ç'est trop schnock !)) mais on ne sait jamais ...

Extrait

"Stratagème 33
"C'est peut-être vrai en théorie, mais en pratique c'est faux." Grâce à ce sophisme, on admet les fondements tout en rejetant les conséquences ; en contradiction avec la règle a ratione ad rationatum valet consequentia (la conséquence tirée de la raison première valide le raisonnement). Cette affirmation pose une impossibilité : ce qui est juste en théorie doit aussi l'être en pratique ; si ce n'est pas le cas, c'est qu'il y a une erreur dans la théorie, qu'on a omis quelque chose, qu'on ne l'a pas fait entrer en ligne de compte ; par conséquent, c'est également faux en théorie."

Documents qui vous ont été adressés par courriel

2008-01-18T11:58:00.000+01:00

J'ai adressé à tous :
- un texte sur la phrase d'Aristote, les ensembles et les relations et le dossier Nabuco
- un texte sur le cas Porte-monnaie
- une spec et exo sur l'administration d'un DESS

Le DS c'est lundi prochain

2008-01-17T22:27:00.001+01:00

Conformément au planning qui se trouve dans le "livret étudiant" distribué en sept 2007.

Les dossiers de TD seront à fournir (comme prévu et comme écrit dans le dossier des sujets) lors de la remise de votre copie.
La règle de notation est écrite dans le dossier des sujets.

Le barème sera fourni sur le sujet. Le corrigé sera fourni via ce bloc-notes. Vous pourrez vous auto-noter. Cela s'appelle la transparence.

Les notes ne sont pas négociables.

La chaire de Gérard Berry au Collège de France

2008-01-17T22:24:00.000+01:00

ICI

Merci à France Culture de nous avoir informé ce matin.

Le Collège de France, créé par François 1er, c'est gratuit. C'est à Paris, mais les confs sont disponibles grâce au web

Esterel, ça rentre dans le cadre de Spec2 que je vais commencer la semaine prochaine.

Ce que j'ai fait lors du cours du 14 janvier

2008-01-15T07:50:00.000+01:00

- J'ai attendu le silence. Que ceux qui viennent en cours comme à la cafet, sèchent mon cours !
Maintenant il est interdit de fumer dans les lieux publics et pas seulement dans l'amphi !

Ils permettront aux étudiants désirant travailler (est-ce travailler que de faire des études ?) de le faire confortablement.

- Le cours détaillé était disponible écrit sur mes pages web et sur le poly et dans mes livres ... j'ai dégagé l'essentiel illustré par des exemples :

- la normalisation des schémas relationnels n-aires (rappel : un tel schéma est un INVARIANT)
: réduire la redondance.
- pourquoi la "4ième forme normale" et la "cinquième" . Définitions et illustrations.
- les opérateurs relationnels : sélection, jointure, projection
- exemples d'arbres de calcul de résultats de requêtes
- et un peu de boxologie : on a mis en boîte ce qui s'écrivait en quelques lignes. D'aucuns appellent de tels dessins des "modèles con ceptuels de données" et des ficelles "relations" comme si quand dans une boite on écrit (N° client, nom, ville) ce n'était pas le schéma d'une relation n-aire !!!
Au fait, nos dessins font partie de la "méthode Merise".

J'ai adressé à tous par courriel, un dossier complet et d'un cas réel : la spéc de l'organisation d'un dess (emplois du temps, intervenants, contrôles, notes, présences) en schémas relationnels n-aire, notation de Ted Codd (prix Turing)

J'ai mis dans le casier de chaque groupe un exemplaire papier de mes pages web sur le modèle relationnel.

Enfin, je vous adresse ce jour, le sujet et le corrigé de mon test en "AGL". Questions comparables vous l'avez vu dans le sujet du ds à venir.

L'informatique et les Indiens

2008-01-10T15:25:00.000+01:00

voir
http://www.voyageindedusud.blogspot.com

Ce que j'ai fait lors du cours du 8 janvier 08

2008-01-10T15:17:00.000+01:00

Comme annoncé, j'ai traité du "modèle relationnel n-aire".
J'ai fait du "conceptuel". Oui oui.
D'aucuns disent que quand on fait des boites et des ficelles c'est "du MCD, modèle conceptuel de données". .. et que quand on fait des parenthèses, c'est du "modèle logique de données, MLT). Foutaises ! Le MCD ne serait pas logique !
Relations, Ensembles c'est conceptuel !
J'ai traité des définitions des "formes normales" de schémas relationnels.
Un schéma relationnel EST UN INVARIANT.
Une "contrainte d'intégrité référentielle" c'est tout simplement une contrainte de sous-ensemble.
Derrière le mot "clé", rien de plus que celui de fonction !

Un schéma en 1ère FN est un schéma qui impose à tous les constituants des relations de prendre leurs valeurs dans des ensembles d'atomes (les SETS de B)...
Le cours est sur le poly et sur les pages web pointées dans un précédent courriel.

Mais bien peu d'étudiants sont allés lire ces pages. J'ai des chiffres !

Voir http://www.lefenetrou.blogspot.com

L'hôtelier, le groom et les clients (où est passé l'euro, suite)

2007-12-18T18:13:00.000+01:00

MACHINE
HCG
SETS
ENTITE ={hotel, client, groom}; TYPE ={input, output}
VARIABLES
solde, montant
INVARIANT
montant : ENTITE * TYPE --> INTEGER &
solde = %ee. (ee : ENTITE montant(ee|-> input) - montant (ee |-> output)) & (
solde(hotel) + solde(client) + solde (groom)) = 0
INITIALISATION
/* solde, montant := ENTITE * {0}, (ENTITE*TYPE) * {0}*/
solde := {(hotel |-> 0),( client |-> 0), (groom |-> 0)}
montant := {((hotel |-> input)|-> 0), ((client |-> input) |-> 0), ((groom |-> input) |-> 0), ((hotel |-> output)|-> 0), ((client |-> output) |-> 0), ((groom |-> output) |-> 0)}
OPERATIONS
transaction(emetteur, recepteur, mt) =
PRE recepteur : ENTITE &
mt : INTEGER &
((mt + montant(recepteur |->input)) <-->output)) > MININT) &
((solde(emetteur) - mt) > MININT)
THEN
solde := solde \/ {(emetteur |-> solde(emetteur) - mt), (recepteur |-> solde(recepteur) + mt)} - {(emetteur |-> solde(emetteur)), (recepteur |-> solde(recepteur))}
montant := montant <+ {((recepteur|-> input) |->(montant(recepteur |->input) + mt)), ((emetteur |->output) |-> (montant(emetteur |-> output)+ mt ))}
END

END
P.S. attention ! certaines fontes ne "prennent" pas le "pipe" (en conséquence, il se peut que le symbole de maplet soit tronqué)

"Quand on cherche les conditions psychologiques du progrès de la science, on arrive bientôt à cette conviction que c'est en termes d'obstacles qu'il

2007-12-18T09:10:00.000+01:00

faut poser le problème de la connaissance scientifique."

On ne connaît que "contre une connaissance antérieure"

"Quand il se présente à la culture scientifique, l'esprit n'est jamais jeune. Il est même très vieux, car il a l'âge de ses préjugés. Accéder à la science c'est, spirituellement rajeunir ..."

"Qui est enseigné doit enseigner"

Gaston Bachelard

Le prochain cours est ici

2007-12-18T08:43:00.000+01:00

Conseils :

ne venez pas en cours si c'est pour roupiller ou platusser ou croiser les bras. Surtout que mon cours a lieu le lundi matin à 8 heures. Économisez de l'énergie, minimisez la pollution.
C'était ma contribution, modeste certes, à la diminution du trou de mémoire, ...d'ozone.
mais étudiez chez vous le cours pré-écrit ici
et si vous avez des questions à poser, alors venez au cours
si vous trouvez confortable une présentation orale et visuelle, alors venez en cours. Écoutez et prenez en notes. Qui scribit bis legit !

P.S. : la dernière partie du DS porte sur ce chapitre.

Histoire du modèle relationnel n-aire

2007-12-18T08:42:00.000+01:00

Lire notre article en mémoire de Robert Mallet

"Le talent c'est d'avoir envie de faire quelque chose"

2007-12-18T08:27:00.000+01:00

"Un homme, c'est pas fait pour bouger, c'est pas fait pour s'arrêter, c'est fait pour continuer, pour mourir en mouvement, mais ce n'est pas fait ...
Tout le malheur vient de l'immobilité. Toujours."

Jacques Brel

Ce que j'ai fait en cours ce 17-12-07, 8h15

2007-12-17T09:35:00.000+01:00

Les 4 sens du verbe "être" d'après Frege
La phrase d'Aristote et la critique de objet/est/attribut
Et la naissance de la chimie avec Lavoisier
La boxologie. Ce n'est pas parce qu'on met dans des boîtes que l'on fait du "conceptuel"
un schéma relationnel "n-aire" à la Codd
et

Notion de séquent : H |- P où H, collection d'hypothèses et P conjecture à prouver. Hypothèses et conjecture sont des prédicats. Ces prédicats peuvent être écrits en utilisant le symbole => (à ne pas confondre avec le tourniquet |- (turnstile en anglais))

H |- P se lit : H entraîne P ou encore Prouver P sous les hypothèses H

exemples :

s <: t, t <: u |- s <: u

|- 0 = 0

Notion de règle d'inférence :

séquent 1

....

séquent n

__________________

séquent

Les séquents au-dessus du trait sont les antécédents de la règle, celui au-dessous est le conséquent de la règle.

Usage de la règle par l'avant : le preuve de séquent dérive de celles de séquent1,..., séquent n. De la preuve de séquent1, ..., séquent n on dérive celle de séquent.

Usage de la règle par l'arrière : on voudrait prouver séquent. On remplace ce but par ceux corrrespondants à la preuve des séquents séquent1, ..., séquent n.

Ne pas confondre le => (implication) Prédicat => Prédicat

avec le |- (entraîne) Prédicat1, prédicat2 - Prédicat3

avec le trait horizontal (de la preuve des séquents, on déduit la preuve du séquent)

Et j'ai fini par :

Les règles de base du raisonnement mathématique :

Hypothèse : si un prédicat fait partie des hypothèses, alors il est prouvé
Monotonie : la preuve d'un prédicat sous certaines hypothèses n'est pas remis en cause par l'ajout d'hypothèses supplémentaires
Coupure : si un prédicat est prouvé sous certaines hypothèses alors ce prédicat peut être ajouté à ces hypothèses si besoin est.

en conseillant aux élèves intéressés par le cours de lire, dans le silence qu'on ne peut obtenir dans l'amphi, le chapitre du poly sur la preuve (ou de me demander le cours en vidéo de J.R. Abrial sur la preuve).

Je voulais aussi rappeler ce qu'est :

la décidabilité
la semi-décidabilité

Mais il y a des messages sur ce bloc-notes qui traitent de cette question du DS

Richard II et Richard III

2007-12-16T18:31:00.000+01:00

Un étudiants m'a signalé que j'avais fait une erreur dans le poly de sujet de TD en indiquant que ma citation venait non de Richard II mais de Richard III de W. Shakespeare. Consultant mes oeuvres "dites complètes" de W.S. j'ai effectivement trouvé Richard III et ai fait un erratum sur ce bloc-notes.
Mais je me suis battu la coulpe trop vite. Ma citation était bien référencée.

The Life and Death of Richard the Second

SCENE III. A royal palace.

Enter HENRY BOLINGBROKE, HENRY PERCY, and other Lords

DUCHESS OF YORK

O king, believe not this hard-hearted man!
Love loving not itself none other can.*

site du MIT (Mass Inst of Technology). http://shakespeare.mit.edu/

* O roi ! ne crois pas cet homme au coeur dur !
Qui ne s'aime pas soi-même ne peut aimer personne.

(traduc d'Hugo)

SETS
PERSON
VARIABLES
loves
INVARIANT
loves : PERSON <--> PERSON
&
dom(loves) - dom (loves /\ id(loves)) = { }
INITIALISATION
loves := { }
END

Brel, Pagny, Camus

2007-12-16T09:57:00.001+01:00

Hier j'ai acheté Noces suivi de L'été d'Albert Camus. Le Monde 2 par ses articles m'avait redonné le goût de Camus.
Hier soir la télé m'a offert un long moment de bonheur. "Heureux comme Dieu en France". F. Pagny chantait Brel et nous présentait des interviews du Grand Jacques. Bravo !

Camus a-t-il rencontré Brel ? Camus est mort en 1960. Je me souviens encore de cette photo en bas à droite de la première du journal où l'on voyait une voiture (une Facel Vega) contre un platane, titrée de la mort de Camus.

Je m'imagine la rencontre des deux hommes.

Quelques citations de Brel :

"Vieillir c'est oublier sa jeunesse"
"Il faut dire Monsieur, que chez ces gens là on ne pense pas"

et de Camus :

"Certes c'est une grande folie, et presque toujours châtiée, de revenir sur les lieux de sa jeunesse et de vouloir revivre à quarante ans ce qu'on a aimé ou dont à fortement joui à vingt. Mais j'étais averti de cette folie" (L'été)

"L'ignorance reconnue, le refus du fanatisme, les bornes du monde et de l'homme, le visage aimé, la beauté enfin, voici le camp où nous rejoindrons les Grecs." (L'été)

"Dans nos plus extrêmes démences, nous rêvons d'un équilibre que nous avons laissé derrière nous et dont nous croyons ingénument que nous allons le retrouver au bout de nos erreurs."

Flûte, je me suis trompé de bloc-notes, je ne suis pas sur http://lefenetrou.blogspot.com/

Au diable les casiers, les modules, les UE, UV et autres disciplines, sections !

Offre d'emploi

2007-12-15T09:35:00.000+01:00

Bonjour Monsieur

Le service logiciel du serviceTrain Control
 Engineering d'ALSTOM TRANSPORT
basé à Meudon La Forêt (92) recherche des
 ingénieurs pour effectuer des 
développements de logiciels de sécurité
pour la signalisation de ses
métros
Profils recherchés ->
- Jeunes diplomés
- Connaissances programmation logiciels
temps réel embarqués
- Logiciels sûrs
- Conception et vérification formelle (méthode B)
- langage ADA, C
Si vous connaissez des candidats ayant un
profil correspondant, n'hésitez
pas à nous envoyer un CV et lettre de motivation
Merci par avance


Jean-René HULOT
Resp. Développement Logiciels Automatic
Train Control
ALSTOM TRANSPORT
Site de Meudon
Jean-rene.hulot@transport.alstom.com

Alstom protège l'environnement :
n'imprimez ce mail que si
nécessaire.
With Alstom, preserve the environment.
Is printing this email really
necessary ?

Mon cadeau de Noël

2007-12-13T09:41:00.000+01:00

ici. Il n'y a pas que le C dans la vie !

Le sujet du DS de Spec1, 2008

2007-12-12T10:37:00.001+01:00

1) voir messages précédents (je sais, il faut les lire !)
2) Contenu :

Des questions sur tous les cours (dont un certain nombre ont leur réponse sur ce blog) et bien sûr une bonne partie du DS indiqué sur mes pages (questions ayant rigoureusement le même énoncé. Mais bien peu d'entre vous ont eu le courage d'aller voir) , le reste étant fort ressemblant et en bonus, ce que j'ai indiqué comme question lors du cours.

Bien sûr il faut avoir compris le petit test de maths. Mais la majorité n'a pas de pb étant donné les notes de maths !

Le barême sera indiqué sur le sujet. Vous pourrez donc vous auto-noter. Nous ne changerons pas le barême "à la tête du client" (pardon, de l'étudiant) : Egalité.

Vous disposez d'autres sujets sur mes pages web spec1.

Combien de mots dans "Le chien mord le facteur"

2007-12-12T10:34:00.000+01:00

1) Définissez ce qu'est un mot pour vous (en termes formels)
2) Donnez un exemple d'un ensemble de mots
3) Répondez à la question en respectant votre définition données via vos réponses à 1) et 2)

Pour le corrigé demandez à lire les notes de TD d'étudiants des groupes 1 et 3.

La plateforme RODIN

2007-12-11T16:54:00.000+01:00

La présentation de J.R. Abrial avec l'étude de cas : clés d'hôtel en B événementiel (lire le chapitre dans le polycop et venir suivre le cours de Spec2)
(après nos clés de coffre-fort, un ex-projet de 2ième année du siècle passé)

http://www.clearsy.com/flash/pdf/rodin_industry_day_2007_sld_abrial.pdf

Notre petit cadeau de Noël

2007-12-11T16:47:00.000+01:00

Demandez votre cle USB au Papa Noel. Voir la Vidéo.

Les test du village (certains étudiants comprendront pourquoi ce message)

2007-12-11T14:07:00.000+01:00

Il fait partie des tests projectifs
comme le Rorschach

Le livre que j'ai chez moi et que j'ai dû faire acheter à la biblio de l'iut est :

Didier Anzieu, Catherine Chabert, Les Méthodes projectives, PUF-Quadridge, 2004, ISBN 2130535364

et un blog que nous aimons bien :
http://www.charlatans.info/tests-d-embauche.shtml

La construction de la boucle (un cours de Marc Guyomard)

2007-12-11T10:27:00.000+01:00

Suite à mon cours sur la construction de la boucle de la recherche du max d'un tableau, voici un excellent texte de mon collègue de l'ENSAT (sur ma page, rubrique Mélange, à la fin de la liste)

Toujours l'inclusion (message au Groupe 3)

2007-12-11T09:46:00.001+01:00

"On attend le corrigé. Si on avait le corrigé, on saurait faire. On comprendrait."

Tiens !

Quand je vois combien d'étudiants sont allés étudier les corrigés sur ce blog ...

Je ne ferai pas un corrigé pour :

- tout chef de service en membre du service dont il est chef
- tout (a|->b) appartenant à R1 appartient à R2
- tout x appartenant à A appartient à B
- tout y appartenant à Y appartient à Z
- tout truc appartenant à MACHIN appartient à CHOSE
- tout (a|->b) |-> c appartenant à TCHOC_TCHOC appartient à TCHOUC_TCHOUC

il y en a déjà assez dans le poly et le cours (proverbes etc.).

Le (CAO) Cerveau Assisté par Ordinateur * est le titre d'un dessin de Zévar célèbre (il y a pas mal d'années):

Années 5O, La 1ère génération : langage binaire
Années 60, La 2ième génération : LDA 6 1
STD 6 1
BRN 14 26
ADD 24 12
Années 70, La 3ième génération : IF A = B GO TO C ELSE PERFORM D.
Années 80 : La 4ième génération : Listez moi tous les articles du stock dont le nom commence par "ANO"
A quand la 5ième ? "Zut je m'souviens plus de c'que j'voulais ! vous pouvez me l'dire ?"

Désolé, je ne suis pas de la 5ième génération !

* et l'Atelier B n'est pas du CAO

La boxologie illustrée

2007-12-11T09:42:00.000+01:00

Dans un prochain cours nous allons traiter du "modèle relationnel n-aire" (étudiez le chapitre dans le poly). "On" (pas nous !) vous dira que c'est "un modèle logique" alors que quand on dessine des boîtes et des ficelles c'est "un modèle conceptuel".

Boxologisons. Facile ! le secret est ici

Variables. Danger !

2007-12-10T10:50:00.000+01:00

Variables, en maths, en informatique. Halte à la confusion !

extrait d'un livre de logique :

« mettre en garde le lecteur contre une interprétation du mot "variable" qui est encore assez répandue, mais qu'il doit bannir de sa pensée. (…)
Nous formalisons l'énoncé suivant :
Si le produit de deux nombres réels quelconques est nul, alors l'un de ces nombres est nul. (1)
en écrivant :

All x All y [(x.y = 0) ? (x = 0 ou y = 0) ]. (2)
Plus d'un lecteur, sans doute, se serait contenté d'écrire
(x . y = 0) ? (x = 0 ou y = 0), (3)
sans quantificateurs. Cela provient, nous semble-t-il, d'une "ancienne version" de la notion de variable, encore assez répandue. Selon cette interprétation, les variables x et y de la proposition(3) désignent — par définition du mot "variable" — des nombres quelconques, donc l'adjectif "quelconques" qui figure dans l'énoncé (1) est déjà traduit dans l'usage de variables x et y dans (3). L'adjonction de quantificateurs, comme dans (2), ne paraît certainement pas fausse, mais en tout cas superflue.
C'est ce sens du mot "variables" que le lecteur de cet ouvrage doit bannir de sa pensée. Le sens qui subsistera est un autre sens, que l'on rencontre aussi et même plus fréquemment que le premier, dans les textes mathématiques. Considérons par exemple les phrases suivantes, que l'on pourrait rencontrer dans un manuel de géométrie.
Soient x et y les longueurs des côtés du triangle rectangle ABC, et z la longueur de l'hypothénuse. On a
z2 = x2 + y2. (4)
Il est clair que dans ce contexte, les variables x, y, z de l'équation (4) n'ont rien de "variable". Elles désignent des nombres particuliers, que l'on ne connaît peut-être pas, mais particuliers tout de même. D'ailleurs l'adjonction de quantificateurs universels All x All y All z à (4) n'entre pas en considération. Elle ne serait pas superflue, mais simplement fausse.
(…)
En lisant une proposition sans quantificateurs telle que (3), le lecteur doit donc s'habituer à considérer les variables qu'elle contient comme désignant des objets particuliers, même s'il ne possède aucune autre information sur ces objets. Le sens des propositions (2) et (3) n'est donc pas le même et les quantificateurs de la première sont indispensables pour traduire (1) » [ZAH 98]

L’indécidabilité de l’infection par un virus

2007-12-10T10:45:00.000+01:00

J-P Delahaye

Définition : un programme infecté est un programme qui en modifie au moins un autre.

Supposons que nous ayons écrit un programme DÉTECTEUR qui indique si un programme donné est un programme infecté ou non, soit le programme PIÈGE défini par :

Si DÉTECTEUR appliqué à PIÈGE donne le résultat oui, alors ne rien faire.

Si DÉTECTEUR appliqué à PIÈGE donne le résultat non, alors choisir un programme dans la mémoire et l’infecter, c’est-à-dire y insérer PIÈGE.

PIÈGE est-il un programme infecté ?

Si la réponse est oui, alors PIÈGE ne fait rien aux programmes et PIÈGE n’est pas un programme infecté, c’est une contradiction.

Si la réponse est non, alors PIÈGE infecte un programme et donc est un programme infecté, ce qui est encore une contradiction. Il en résulte que DÉTECTEUR ne peut exister.

Conclusion : il n’existe pas de détecteur universel de programmes infectés. »

J-P Delahaye in Logique, informatique et paradoxes, Pour la science, Belin, ISBN : 2-9029-1894-1

Rappel : la logique des prédicats d'ordre deux est semi-décidable. Comme vous savez que par exemple l'inclusion se définit avec un tel prédicat ... il vous faut savoir que l'on ne peut avoir de prouveur décidable. Il n'est que semi-décidabe. Lire poly.

Des fondamentaux, indécidabilité, etc...

2007-12-10T10:44:00.000+01:00

ici

encore une partie des réponses de questions du DS à venir !

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

2007-12-10T10:33:00.000+01:00

Un exemple allant de la spec à l'IMPLEMENTATION (l'opération maximum d'un tableau)
avec la construction de la boucle WHILE DO INVARIANT VARIANT END
avec utilisation de la substitution "devient tel que" ( x : P)

un complément aux clauses d'une machine avec le PROMOTES et l'EXTENDS pour l'INCLUDES (illustration par des dessins, cas Coffres bancaires)

Enseignement, j'ai cité France culture de dimanche matin, écouté alors que je mettais au point le sujet du ds en latex.

Commandes latex pour B

2007-12-09T20:52:00.000+01:00

Nous donnons le code ASCII et en face la commande Latex

: \in
/: \notin
<: \subseteq
/<:
><
=> \implies
% \lambda
; \comp
\/ \cup
/\ \cap
& \land
or \lor
! \forall
# \exists
--> \fun
+-> \pfun
>--> \bij
<--> \rel
|-> \mapsto
|> \rres
<| \dres
||> \nrres
<|| \ndrres
>+-> \pbij
+->> \psurj
>+-> \pinj
-->> \surj
>--> \inj
== \defs
<-- \leftarrow
|| \parallel
/= \neq
<= \leq
{} \emptyset
* \times (produit cartésien)

Le problème des étudiants aujourd’hui

2007-12-08T08:50:00.000+01:00

« En informatique, la tentation d’imprimer
beaucoup et de 
réfléchir peu est inquiétante. (…)
Le problème des étudiants 
aujourd’hui, c’est qu’ils ne lisent
pas de livres »

Pierre-Gilles 
de Gennes, cité par C-X. Durand in
La nouvelle guerre contre 
l’intelligence, Isbn : 2-86839-734-4

Information aux étudiants qui dorment en TD et en cours

2007-12-07T18:27:00.001+01:00

Lors du recyclage Secouriste Sauveteur du Travail (SST) hier a-m la formatrice a rappelé que :

Si un étudiant dort pendant un ds, td, cours, le SST doit impérativement le réveiller. Si l'étudiant ne se réveillait pas (ex: crise cardiaque) à la fin de la séance, le SST présent serait en faute grave. Et on le voit mal au tribunal raconter que c'est normal que les étudiants roupillent en cours et en td.

"Le vrai Paradis de Platon

2007-12-06T18:46:00.000+01:00

ou comment Einstein, Gödel et les autres nous éclairent sur les limites de la connaissance"
John L. Casti, Le Pommier, 2005

Perelman et sa preuve

2007-12-06T10:01:00.000+01:00

Lire ici

Shakespeare n'a pas écrit Richard II, mais Richard III

2007-12-06T09:29:00.000+01:00

merci à l'étudiant qui nous a signalé cette erreur dans le poly des td de spec1. A corriger.

"Le sujet de Richard III, la marche impitoyable de Gloucester vers le trône par dessus les cadavres, son triomphe et sa chute, est la suite immédiate de la troisième partie d'Henri VI" (W.S. Oeuvres théâtrales complètes)

Sujet du DS à venir (suite)

2007-12-04T10:25:00.000+01:00

Sur la numération, de belles pages en couleur (mieux que mon poly en noir et blanc)

ici (merci à son auteur)

Rendez-vous à Budapest

2007-12-04T09:27:00.000+01:00

Ici

Effet paillasson, effet bi-standard

2007-12-04T09:05:00.000+01:00

"Faites un rapide sondage des réponses à la question suivante : ``La caution de la science en faveur du paranormal constituerait-elle un argument de poids en faveur de celui-ci ?'' Vous obtiendrez, à n'en pas douter, un ``oui'' quasi unanime. Posez une seconde question à ces mêmes personnes que vous venez d'interroger il y a seulement quelques instants : ``Si la science rejetait le paranormal, cela entamerait-il votre adhésion à celui-ci ?'' Et vous obtiendrez un ``non'' également quasi unanime. En d'autres termes, vous présentez votre demande d'adhésion à un club ; s'il vous accepte, c'est un bon club ; s'il vous refuse, c'est un mauvais club.''

Georges Charpak, Henri Bloch, Devenez sorciers, devenez savants, Odile Jacob, 2002, ISBN : 2-7381-1093-2

Exercice d'application :

Vous fournissez une copie à un prof, s'il vous met 18 c'est un bon prof, s'il vous met 4 c'est un mauvais prof.

Et je propose que les bons profs voient leur pouvoir d'achat augmenté et que ce soient les étudiants qui notent les profs.

J'assure une montée du niveau des notes.

On peut observer là où cela se pratique....

Et si on appliquait cela à la médecine. Ca va pas la tête ! on passe tous entre les mains d'un médecin un jour ou l'autre !

effet bi-standard :

cet effet consiste à modifier les règles du jeu en fonction des réponses ou en fonction des joueurs

Exercice d'application :

Vous connaissez des tas d'applications ...

effet paillassion :

effet qui consiste à utiliser un mot pour désigner autre chose que ce que ce mot désigne. Vous êtes surpris par le drôle de nom de cet effet ? Vous ne l'oublierez plus lorsque vous aurez constaté avec nous que, contrairement à ce que demande l'écriteau qui accompagne un paillasson, à savoir ``Essuyez vos pieds SVP'', vous n'avez vraisemblablement jamais enlevé vos chaussures et vos chaussettes pour vous essuyer les pieds ! CQFD''

Georges Charpask, Henri Bloch, Devenez sorciers, devenez savants, Odile Jacob, 2002, ISBN : 2-7381-1093-2

M. Jackson (pas lui, l'autre, l'auteurs de JSP (Jackson Software Programming), JSD (Jackson Software Development)) a dans un de ses livres donné un autre exemple.

Vous l'avez lu dans le poly dont vous disposez.

2007-12-03T18:48:00.000+01:00

Outils de ClearSy/Méthodes

ClearSy réalise des outils d'ingénierie et distribue notamment l'Atelier B, B4free, Brama et CompoSys. D'autres outils sont en cours de développement.

	CompoSys, version 1.6 CompoSys est un outil de modélisation de système. Sa nouvelle version, la version 1.6, est maintenant compatible avec les outils OPEN SOURCE Rodin, et présente les fonctionnalités suivantes : Editeurs machine et dictionnaire : Les éditeurs sont remplacés par des éditeurs à base de formulaires. Vues supplémentaires : Une vue pour la description longue. Une vue pour le graphe des liens entre composants. Nouvelles fonctionnalités : Les systèmes peuvent être prouvés directement sous Composys. L’animation des modèles est également disponible. Cette nouvelle version sera prochainement diffusée. Nous ne manquerons pas de vous en informer... Pour en savoir plus, rendez-vous sur le site CompoSys.fr.

	BART Le projet BART (B Automatic Refinement Tool) vise à développer un outil de raffinement automatique de machines B. Cet outil permettra de générer automatiquement une implémentation B0 pour une machine ou un raffinement B suffisamment détaillé. BART fonctionne sur une base de règles de raffinement. Des règles de raffinement supplémentaires peuvent être ajoutées afin de permettre la personnalisation du raffinement de certains composants. L'outil de raffinement automatique BART est développé dans le cadre du projet européen RIMEL, et sera intégré dans la prochaine version de l'Atelier B. La spécification est actuellement en cours de finalisation...

	Le traducteur ComenC Le traducteur ComenC est un nouveau traducteur pour le langage B. Il permet de traduire des implémentations B0 vers le langage C. Ce traducteur est issu de la convergence entre les traducteurs industriels, et des travaux de recherches tels que le projet RNTL BOM (B optimisé mémoire). Par rapport aux traducteurs précédents, le traducteur ComenC propose une traduction plus simple, permettant d'obtenir un code plus efficace et plus proche du B0 d'origine. Le traducteur C ComenC est maintenant fourni avec B4free, et sera prochainement distribué sous licence "open-source". Nous ne manquerons pas de vous informer des évolutions à venir de l'outil...

Nos Produits et Formations

Appartenance, Ensemble des sous-ensembles, Ensemble des relations, Produit cartésien

2007-12-03T12:22:00.000+01:00

Le test a été communiqué au prof de maths. Il a 20/20. C'était bien des maths ! Ouf !

Mais il est quand même pratique d'utiliser les abréviations de la notation B pour avoir des spécs
plus concises.

Il y a huit mots dans cette phrase, Il n'y a pas huit mots dans cette phrase

2007-12-03T12:07:00.000+01:00

MACHINE
phrasesParadoxales
/* Le contraire d'une vérité n'est pas toujours un mensonge :
"Il y a huit mots dans cette phrase". Vrai.
"Il n'y a pas huit mots dans cette phrase" Vrai aussi !
La traduction de ce texte en anglais constitue cette fois deux
mensonges au lieu de deux vérités :
There is eight words in this sentence. Faux.
There is not eight words in this sentence. Faux aussi !*/
SETS
MOT ={il, y, a, huit, mots, dans, cette, phrase,n', pas}
CONSTANTS
phrase1, phrase2
PROPERTIES
phrase1 : seq(MOT) & phrase2 : seq(MOT) &
phrase1 =[il, y, a , huit, mots, dans, cette, phrase] &
phrase2 = [il, n', y, a, pas, huit, mots, dans, cette, phrase]
bool(card(dom(phrase1))=8) = TRUE &
bool(card(dom(phrase2))=8) = FALSE &

bool(not(card(dom(phrase1))=8)) = TRUE

END

/* Cette machine ne passe pas la phase de Type Check sur l'Atelier B car il y a des identificateurs qui ont moins de 2 caractères */

/*La spéc suivante passe la phase de type check. Mais quand on lance la génération des OP, on
obtient le message suivant : STRING type can only be used to type operations input parameters,
with the belong predicate */
Nota : ne mettez pas d'accents dans les commentaires d'une spéc que vous voulez conduire jusqu'au code ADA, voir les conseils sur un précédent message.

MACHINE
phrasesParadoxales
/* Le contraire d'une vérité n'est pas toujours un mensonge :
"Il y a huit mots dans cette phrase". Vrai.
"Il n'y a pas huit mots dans cette phrase" Vrai aussi !
La traduction de ce texte en anglais constitue cette fois deux
mensonges au lieu de deux vérités :
There is eight words in this sentence. Faux.
There is not eight words in this sentence. Faux aussi !*/

CONSTANTS
phrase1, phrase2, mots
PROPERTIES
mots <: STRING & mots = {"il"," y", "a", "huit", "mots", "dans", "cette", "phrase","n'", "pas"}
phrase1 : seq(mots) & phrase2 : seq(mots) &
phrase1 =["il"," y", "a", "huit", "mots", "dans", "cette", "phrase"] &
phrase2 = ["il", "n'"" y", "a", "pas", "huit", "mots", "dans", "cette", "phrase"]
bool(card(dom(phrase1))=8) = TRUE &
bool(card(dom(phrase2))=8) = FALSE &

bool(not(card(dom(phrase1))=8)) = TRUE

END

"Je ne comprends pas les Anglais

2007-12-03T12:02:00.000+01:00

MACHINE
vaincusVainqueurs
/*Je ne comprends pas les Anglais ! Tandis qu'en France nous donnons à nos rues des noms de victoires : Wagram, Austerlitz… là-bas, on leur colle des noms de défaites : Trafalgar Square, Waterloo Palace… (Alponse Allais)"
SETS
PAYS; LIEU; DATE
VARIABLES
aBattuA
DEFINITIONS
victoires(pp) == ran({ (xx|->yy)|->zz) | (xx|->yy)|->zz) : dom(aBattuA) & (xx =pp)});
defaites(pp) == ran({ (xx|->yy)|->zz) | (xx|->yy)|->zz) : dom(aBattuA) & (yy =pp)})

INVARIANT
aBattuA : (PAYS * PAYS) * DATE +-> LIEU
/* le pays x a battu le pays y à la date d au lieu l */
INITIALISATION
aBattuA :={}
END

/* Alphonse Allais avait bien compris qu'une date n'est pas plus une date de naissance qu'une date de décès, que 3 rue Ml Joffre est l'adresse postale du département informatique de l'IUT de Nantes mais aussi l'adresse du lieu où vous avez glissé sur une peau de banane, que Nantes n'est pas plus une ville de décès qu'une ville de naissance, etc. */
/* Alors ne spécifiez pas ainsi :
SETS
DATE_De_NAISSANCE; DATE_De_DECES
ou encore
PISTE_OCCUPEE; PISTE_Non_OCCUPEE

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

2007-12-03T10:08:00.000+01:00

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.

Le site consacré à E. Dijkstra

2007-12-02T21:51:00.000+01:00

ICI

Les pages d'un collègue de Bordeaux

2007-12-02T21:03:00.000+01:00

Ici

voir aussi sa liste de problèmes rencontrés avec l'Atelier B

... et les pages B du site mondial des méthodes formelles

Modèle ? et indécidabilité

2007-12-02T10:09:00.000+01:00

La lampe de Thomson (toujours un extrait du livre de Boulanger et Cohen, Le Trésor des paradoxes, Belin, 2007. Une mine. Mais je suis sûr que vous l'avez déjà acheté)

"Une lampe reste allumée une minute, éteinte une demi-minute, rallumée un quart de minute, et ainsi de suite indéfiniment.

( Rappel : en B, on se méfie de l'infini. Les SETS sont des ensembles finis. Et on doit prouver qu'une boucle se termine... Ce sera le cours de la semaine à venir)

La série (1 + 1/2 + 1/4 + 1/8 + ...) converge vers 2. Dans notre cas, 2 minutes.

On s'attend donc à ce que la lampe soit allumée ou éteinte, après ce cycle d'allumages et d'extinctions successifs.
Mais l'état de la lampe est indécidable, car il est impossible de préciser si l'interrupteur se trouve ou non enclenché au terme d'un nombre infini de poussées, vu qu'il n'existe pas de dernière poussée ! "

Contexte

2007-12-02T09:13:00.000+01:00

En B, nous donnons le contexte avec la déclaration des SETS, CONSTANTS et VARIABLES et avec les commentaires (essentiels). Les DEFINITIONS sont aussi très utiles.

"Rappelons que les lois physiques n'ont pas de valeur de vérité absolue, mais relatives à des conditions explicites.
Ainsi, la formule "l'eau bout à 100°C et gèle à 0°C" n'est vraie qu'à la pression habituelle d'une atmosphère."

(voir l'expérience du "bouillon de Franklin")

Quand vous spécifiez :

n'oubliez pas de spécifier si vos entiers représentent des pieds ou des mètres, des dollars ou des euros, des degrés celsius ou fahrenheit, des minutes ou des heures, etc.
si vos éléments de votre SET LIVRES sont ce qu'identifient les ISBN ou ce qu'identifient les n°s d'inventaires à la bibliothèque de l'IUT
si votre relation Emprunts représente les emprunts en cours ou l'historique des emprunts

N'oubliez pas d'apprendre mon cours sur les échelles de mesure (voir mon livre La mesure du logiciel). Si vous utilisez une échelle ordinale vous ne pouvez faire les opérations que vous faites avec une échelle absolue. On distingue les types d'échelles suivantes : nominale, ordinale, ratio, intervalle, absolue

S'il fait 10° C ça NE veut pas dire qu'il fait deux fois plus chaud que quand il fait 5° C.

Quand il y a 100 étudiants présents dans l'amphi, il y a deux fois plus d'étudiants que lorsqu'il y a 50 étudiants présents dans l'amphi.
Quand on a prévu 1 homme-mois pour développer tel programme, cela peut être réalisé avec 2 hommes pendant 15 jours ou 5 hommes pendant 6 jours. C'est comme 10 m2. Ce peut être 10 carrés d'un m2 ou 2 carrés de 5 m2.

D'après vous, les notes données par les enseignants font référence à quel type d'échelle ?
Quel est le type d'échelle sous-jacent aux échelles Fahrenheit, Celsius ?
voir http://fr.wikipedia.org/wiki/Fahrenheit

Images avec Latex

2007-12-01T10:46:00.000+01:00

Bonjour,

Le fichier Latex du poly de spec que
vous m'avez donné fonctionne très
bien. Cependant j'ai un problème lorsque
je veux insérer un fichier image:
le .pdf affiche bien la légende, mais
l'endroit où est censée se situer
l'image reste blanc.
Voici ce que je tape, suivant votre
modèle:

\begin{figure}
\centering
\epsfig{file=relationQuelconque.eps,width = 5cm}
\caption{\label{relationQuelconque}
Relation Quelconque}
\end{figure}

Mon image est au format .eps (éditée
sous Photoshop), en mode ASCII, et je
l'ai placée dans le même dossier que
mon fichier .tex. J'utilise bien le
pack "epsfig".

Si vous connaissez la solution à mon
problème, je suis preneur...
Bon WE

_____________
Ma réponse :
Dans le poly je n'ai pas eu de pb pour
mettre la photo du soroban.
Mais je n'ai pas réussi à mettre celle
du boulier russe.
Je n'ai pas la réponse. Je vais consulter
des spécialistes de Latex à la fac.
A suivre.
Si un autre étudiant a la réponse merci
à lui de la communiquer sur ce blog. Pour tous.

La preuve de Dionysodore

2007-12-01T10:19:00.000+01:00

" Conviens-tu que ton père est à la fois le tien et père ?
- Bien sûr,
- Bon. As-tu un chien ?
- Oui.
- Et a-t-il eu des chiots ?
- Certes, car je l'ai vu saillir la chienne qui a mis bas.
- Etant ainsi à la fois le tien et père, ce chien est donc ton père ! "

Les sophistes de Mégare ont pu s'amuser à ces sophismes ... on n'avait pas encore inventé les relations. Eh oui ! il en a fallu des siècles pour les inventer.

La preuve de l'existence de Dieu

2007-12-01T10:10:00.000+01:00

La preuve ontologique de St Anselme

"Dieu est un être parfait
Or l'existence fait partie intégrante de la perfection
Donc Dieu existe, car s'il n'existait pas il ne serait pas parfait, et s'il n'était pas parfait il n'existerait pas"

"On pourrait renverser la "preuve ontologique" en affirmant que l'inexistence est aussi une qualité intégrée à la perfection, ce qui rappelle la démarchee d'Andrew Wiles : pour démontrer le grand théorème de Fermat, il envisage l'existence d'une courbe elliptique dotée de propriétés si remarquables qu'elle ne peut exister ! "

Boulanger, Cohen, ouv. cité, p. 252

"L'imbécile croit qu'il

2007-12-01T09:54:00.000+01:00

n'existe aucun ensemble vide. Mais s'il en était ainsi, alors l'ensemble de tous les ensembles vides serait vide, et par conséquent, cet ensemble serait l'ensemble vide"

Van Fraasen, rédacteur en chef du Journal de logique philosophique cité par Boulanger et Cohen, p. 301

Au fait, en B il y a plusieurs ensembles vides.

Exemples :

SETS
COURS, PROF
VARIABLES
coursOuverts, profsEnPoste, enseignePar
INVARIANT
coursOuverts <: COURS &
profsAffectes <: PROFS &
enseignePar : coursOuverts +-> profsEnPoste
INITIALISATION
coursOuverts, profsEnPoste, enseignePar := {}, {}, {}

Je NE peux écrire que suite à cette initialisation :

coursOuverts = profsEnPoste &
enseignePar = profsEnPoste

Voir le concept d'ensemble de base (SETS).

Puisque je viens d'apprendre qu'il est demandé aux profs de maths

2007-12-01T09:22:00.000+01:00

en lycée de ne plus apprendre à raisonner et à ne plus apprendre à prouver ...
puisqu'il suffit de "mettre les élèves sur machine" et de laisser jouer l'intuition.

voici quelques extraits de l'EXCELLENT "Le trésor des paradoxes" de Philippe Boulanger et Alain Cohen, Belin, 2007. A acheter, à offrir. Et à lire !

L'homme a tout ce qu'il n'a pas perdu
Il n'a pas perdu de cornes
Donc il a des cornes !

Tous les chats sont mortels
Or Socrate est mortel,
Donc Socrate est un chat !

La ponctualité est la politesse des rois
Or je suis le roi des retardataires ;
Donc je suis toujours ponctuel !

Faites aux autres ce qu'ils devraient vous faire, mais ne vous font pas

C'est lorsque je suis stressé que je fume le plus. C'est lorsque je ne fume pas que je suis le plus stressé

Aujourd'hui je conduis alors je n'ai pas le temps de regarder les panneaux

"Les hommes acceptent de tout assumer, sauf les responsabilités" Oscar Wilde

"Si vous voulez vivre longtemps, vivez vieux" Erik Satie

"Suicidez-vous jeunes, vous profiterez mieux de la mort !" Pierre Dac

Et ces questions d'examen :

Tracer plusieurs cercles de formes différentes
Décrivez la pose de la première pierre des ruines du Parthénon

Au groupe 3

2007-11-30T18:21:00.000+01:00

Ce matin on a fait une erreur.

Pour l'exercice 3.5 Aidez le, l'opération
Inscription(pp,ll)
était bien erronée. Il n'y avait pas que l'opération AjoutCorrection(pp,ll)

Pourquoi ?

On ne s'est pas assuré que l'étudiant pp n'était pas corrigé par le lycéee ll.

(même raison que pour l'opération que nous avons corrigée)

Etonnant !

2007-11-30T17:36:00.000+01:00

J'ai pu constater que des étudiants ne pouvaient répondre ou répondaient de manière erronée aux questions suivantes :

Pour éviter que d'aucuns disent que B utilise des symboles non utilisés par les profs de maths, j'ai proposé de se limiter à (notation ASCII):
: (appartenance)
POW (Ensemble des sous-ensembles d'un ensemble, Power set en anglais)
* (produit cartésien)

Fini le <: (inclusion) etc etc Alors écrire ce qui suit sans utiliser le <: et le <--> :

a <: S
a : A <--> B

Bien sûr les réponses sont dans le poly !

Obtenant des réponses farfelues, j'ai demandé la définition du produit cartésien et de POW. Ouh la la....

Alors voici encore mais cette fois en couleur ....

a : POW(S)
b : POW (A*B)

J'ai déjà fait remarquer à ceux qui ont utilisé l'Atelier B, que ce dernier réécrivait sous cette forme. On voit cela dans les obligations de preuve.

J'ai du revenir sur cela car je traitais d'un exo du poly des td.
Il y a dans le poly de td un exo (la spec qu'un étudiant avait envoyé sur le forum de B) avec

binome : POW(ETUDIANT)
J'ai posé la question : binome est une variable qui a pour valeur 1 binome ? Un ensemble de binomes ?
groupe : POW(binome)
annee : POW(binome)

Si vous avez déjà oublié le cours de maths (pourtant les étudiants m'ont dit avoir eu 18, 15 et 17 au DS !), prenez un exemple ....

et rappel :
si à gauche du signe appartient il y a un ensemble de trucs, à droite il y a un ensemble d'ensembles de truc
si à gauche du signe appartient il y a un ensemble d'ensemble de trucs, à droite il y a un ensemble d'ensembles d'ensembles de trucs

j'ai déjà écrit cela plusieurs fois ici. Voir mes pages web sur B. Avec des exemples en extension.

P.S. : Pour les étudiants qui on séché le TD. Il vous est vivement conseillé d'étudier votre cours de maths et les notes de td des présents.

Les mathématiques arabes : comprendre la constitution des mathématiques classiques.

2007-11-30T17:32:00.000+01:00

Je vous communique ce message. Vous y verrez que la conférence parle de ce dont je vous ai

parlé lors du dernier cours sur la numération.

L'association "Sciences en tête" vous invite à assister à une conférence ouverte à tous le 6 decembre 2007 à 15h30 dans l'amphi A de
la Faculté des Sciences et des Techniques.

Les mathématiques arabes : comprendre la constitution des mathématiques classiques.
Hélène Bellosta

L’intérêt pour l’histoire des mathématiques arabes (/i/. /e/. écrites en
arabe) ne saurait être confondu avec un intérêt de type ethnographique,
mais est un intérêt épistémologique et historique, portant sur l’origine
et l’évolution des concepts fondamentaux constitutifs de la /Mathesis
Universalis/. L’apport des mathématiques arabes est en effet essentiel
pour qui veut comprendre comment se constituent aux XVI^e et XVII^e
siècles les mathématiques classiques. A partir du viii^e siècle en
effet, une vaste partie du monde — de l’Andalousie aux confins de la
Chine et de l’Inde, en passant par le Maghreb, l’Égypte, le Moyen-Orient
et l’Iran — devient le lieu d’une intense activité scientifique dont la
langue est l’arabe. En quelques siècles, les savants de ce monde,
poursuivant l’œuvre de leurs prédécesseurs gréco-hellénistiques, vont
inventer l’algèbre et l’appliquer à toutes les autres branches des
mathématiques, développer, à la suite d’Archimède, les recherches sur
les mathématiques infinitésimales, préparant ainsi les travaux modernes
en théorie de l’intégration, créer, en liaison avec l’optique et
l’astronomie, les nouveaux chapitres de géométrie que sont la théorie
des projections et l’étude des propriétés focales des coniques, jeter
les bases de la trigonométrie. Ce sont, à partir du xii^e siècle, les
traductions latines de certaines de leurs œuvres qui vont faire
découvrir à l’Europe le calcul indien et l’algèbre, entre autres,
préparant ainsi l'essor intellectuel de la Renaissance.

On évoquera au cours de cet exposé quelques grands traits de ces
mathématiques :

1. le rôle de l’algèbre — apport le plus novateur, le mieux connu et le
plus célèbre, des mathématiciens de langue arabe — qui va, en quelques
siècles, se développer de façon spectaculaire, irriguer toutes les
disciplines mathématiques, et créer entre elles des liens jusque là
inexistants ;

2. les calculs d’aires et de volumes (/i/. /e/. les mathématiques
infinitésimales) dans la postérité des travaux d’Archimède ;

3. les nouveaux développements de la géométrie impulsés par l’astronomie
et l’optique.

Hélène Bellosta est ancienne élève de l'École normale supérieure
(Sèvres), agrégée de mathématiques,
detient une maîtrise d'arabe classique, est docteur en épistémologie
histoire des sciences.
Elle a été pensionnaire scientifique à l'Institut d'études arabes de
Damas, et est actuellement
directeur de recherches honoraire au centre d'histoire des sciences
et des philosophies arabes et médiévales.

An example with SEES and INCLUDES

2007-11-28T17:16:00.001+01:00

MACHINE
trucContexte
SETS
AA
END

MACHINE
trucM1
SEES
trucContexte
VARIABLES
var
INVARIANT
var <: AA
INITIALISATION
var := AA
OPERATIONS
trucM1op =
ANY ens WHERE ens <: AA THEN
var := ens
END
END

MACHINE
trucM2
INCLUDES
tien.trucM1, mon.trucM1
OPERATIONS
optrucM2 =
BEGIN
tien.trucM1op ||
mon.trucM1op
END
END

Type check and proofs ok with Atelier B

Composition with SEES and INCLUDES

2007-11-28T17:16:00.000+01:00

Machines with parameters (SETS and scalar) and INCLUDES

2007-11-28T17:13:00.000+01:00

MACHINE
trucM4(AA, maxe)
CONSTRAINTS
maxe : 5..10 &
card(AA) >maxe

VARIABLES
var
INVARIANT
var <: AA & card(var) < trucm1op =" ANY" style="font-weight: bold;">MACHINE
trucM5(AA,maxe)
CONSTRAINTS
maxe : 5..10 & card(AA)> maxe
INCLUDES
tien.trucM4(AA, maxe), mon.trucM4(AA, maxe)
OPERATIONS
optrucM2 =
BEGIN
tien.trucM1op ||
mon.trucM1op
END
END

Type check and proofs ok with Atelier B

The factorial function

2007-11-28T17:10:00.000+01:00

MACHINE
Factorielle
/*encapsule la fonction factorielle */
CONSTANTS
laFactorielle
PROPERTIES
laFactorielle : NAT --> NAT &
laFactorielle (0) = 1 &
! nn. (nn: NAT1 => laFactorielle (nn) = nn * laFactorielle (nn-1))
END

MACHINE
MaFactorielle
SEES
Factorielle
/* cette machine offre une operation qui appelle la fonction factorielle en lui passant le nombre dont on veut la factorielle. C'est une application de fonction */
OPERATIONS
reponse <-- fact(nn) =
PRE
nn : NAT
THEN
reponse := laFactorielle(nn)
END
END

The bool operator of B (transforming a predicate into an expression)

2007-11-28T17:07:00.000+01:00

Où l'on voit bien la définition de bool

MACHINE
essaiBool
VARIABLES
xx, yy, b1, b2
INVARIANT
xx : 0..5 & y : 0..5 &
xx = yy &
b1 : BOOL & b2 : BOOL & b1 = b2
INITIALISATION
ANY truc WHERE truc : 0..5 THEN
xx := truc ||
yy := truc
END ||
b1:= TRUE ||
b2:= TRUE
OPERATIONS
modif(ee) =
PRE
ee : 0..5
THEN
xx := ee ||
yy := ee
END;
verite=
BEGIN
IF (xx=yy) THEN b1:= TRUE ELSE b1 := FALSE END||
b2 := bool(xx=yy)
END
END