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

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

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

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

Lire notre article en mémoire de Robert Mallet

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

"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

• 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

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

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

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

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

Le sujet du DS de Spec1, 2008

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"

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

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

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

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

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)

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)

"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

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 !

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

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

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)

• 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

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

« 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

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

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

Lire ici

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

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)

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

ici (merci à son auteur)

Rendez-vous à Budapest

Ici

Effet paillasson, effet bi-standard

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

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

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

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

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)

• 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

ICI

Les pages d'un collègue de Bordeaux

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é

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

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

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

" 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

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

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

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

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 !

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.

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

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

Machines with parameters (SETS and scalar) and INCLUDES

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

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)

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

Refinement in B (an example)

MACHINE
swap
VARIABLES
xx, yy
INVARIANT
xx : NAT & yy : NAT
INITIALISATION
xx :: NAT ||
yy :: NAT
OPERATIONS
echange =
BEGIN
xx := yy ||
yy := xx
END
END

REFINEMENT
swapR
REFINES
swap
VARIABLES
xr, yr, zr
INVARIANT
xr= xx & yr = yy & zr : NAT
INITIALISATION
xr, yr, zr:= 0, 0, 0
OPERATIONS
echange =
BEGIN
zr := xr;
xr := yr;
yr := zr
END
END


Type check and proofs OK with Atelier B

Le cinquième cours

portera sur :

• la clause REFINES et la machine REFINEMENT
  

• quelques raffinages (vous les trouverez dans le poly)
  

• la boucle, INVARIANT et VARIANT de boucle
  
• le théorème à prouver pour la boucle
  

On sera alors en pleine programmation.

Il nous restera les machines IMPLEMENTATION
celles que l'Atelier B transforme automatiquement en programmes en langage C ou en ADA ou en ...

Devoir chez soi, le corrigé

Université de Nantes
IUT de Nantes
Département informatique
SPEC1
H. Habrias
NOM : PRENOM : Groupe :
__________________________________________________________________________________________
Considérez l’extrait suivant d’une machine abstraite B

SETS

PERSONNE ; SUJET

VARIABLES

professeurs, sujets, enseigne

INVARIANT

professeurs : POW (PERSONNE) &
sujets : POW (SUJET) &
enseigne : PERSONNE +-> POW (SUJET)

Nous allons énoncer des contraintes supplémentaires.
Et fournir plusieurs spécifications, certaines étant mal typées.

Si une phrase à spécifier vous apparaît comme ambiguë, explicitez l’ambiguïté, fournissez une nouvelle rédaction et la spécification associée.

Question 1

« Les personnes qui enseignent sont des professeurs »

Sera exprimé au mieux par :

1.1. dom (enseigne) < : professeurs
1.2. professeurs < : dom (enseigne)
1.3. ran (enseigne) < : professeurs
1.4. dom(enseigne) = professeurs
1.5. aucun des prédicats ci-dessus

1.1

certains ont pu interpréter comme 14

Question 2

« Tous les sujets sont enseignés par les professeurs » (N.B. : nous ne désirons pas dire que chaque professeur enseigne tous les sujets. Nous désirons dire qu’il n’y a pas de sujet qu’aucun professeur n’enseigne. »

Sera exprimé au mieux par :

2.1. ran (enseigne) < : sujet
2.2. enseigne : PERSONNE --> POW (SUJET)
2.3. enseigne : professeurs --> sujets
2.4. aucun des prédicats ci-dessus

2.4

Spécification

enseigne : professeurs -->> sujets

Question 3

« Tous les professeurs ne doivent pas enseigner, sachant que seuls les professeurs peuvent enseigner. »

Sera exprimé au mieux par :

3.1 dom (enseigne) = professeurs
3.2 dom (enseigne – professeurs) /= {}
3.3 professeurs – dom (enseigne) /= {}
3.4 aucun des prédicats ci-dessus

3.3

Question 4

« Un groupe est un ensemble de personnes »

Sera exprimé au mieux par :

4.1 PERSONNE : groupe
4.2 groupe : PERSONNE
4.3 groupe : NAT <-->PERSONNE
4.4 aucun des prédicats ci-dessus

4.5

Spécification

groupes <: POW(PERSONNE)

Question 5

« Une année est un ensemble de groupes »

Sera exprimé au mieux par :

5.1 groupe : année & année < : PERSONNE
5.2 année : POW (groupe) & groupe : POW (PERSONNE)
5.3 groupe < : année & année < : PERSONNE
5.4 aucun des prédicats ci-dessus.

5.4

Spécification
groupes <: POW (PERSONNE) &
annees <: POW (Groupes)


Ce travail est un travail individuel.
De telles questions seront posées en DS. Le corrigé vous sera fourni sur ce bloc-notes.

C'est fait. J'espère ne pas avoir écrit de co(q)uille !


Comme indiqué en cours, il vous faut :

• mettre votre copie dans votre dossier de td dans une annexe
• et sur votre copie, expliquer le pourquoi de vos erreurs éventuelles

Je prendrai en compte ce travail dans la note finale de TD.

Je suis prêt à recevoir tout exercice que vous aurez fait pour vous en fournir un corrigé (mais sur réception de votre travail !)

Ce que j'ai fait au 4ième cours, ce jour

Comme prévu : le raffinage

• J'ai donné une partie du sujet de l'examen (oui, oui) : implantation d'entiers sur un boulier de 4 tiges avec 4 boules par tige
• J'ai montré l'implantation d'entiers sur le boulier japonais (soroban)
• J'ai "montré" le théorème du raffinage sur un exemple (avec réduction de l'indéterminisme) - j'ai donné une illustration de l'indéterminisme sur un petit automate pour le petit cas illustratif utilisé -
• J'ai rappelé comment on passe du quantificateur universel au quantificateur existentiel par la double négation
• J'ai fourni et instancié le théorème du raffinage;
• Pour du raffinage par affaiblissement des préconditions, voir polycopié
• Pour raffinage par remplacement du || avec donc introduction du séquencement, voir livres, poly etc etc ou même cassettes vidéo
• J'ai ramassé le devoir à faire chez soi.
  

Programmeur

lire ceci

Une belle illustration

Merci à Sebastien pour m'avoir fourni ce pointeur.

Rappel. Vous disposez du cours en vidéo

cassettes et magnétoscope à la bibliothèque.

Si vous voulez en en emprunter, me le demander.


C'est le cours fait par J.R. Abrial, l'auteur de B

Pour le cours de demain...

Merci aux représentants de groupes de compiler les copies du devoir pour leur groupe.

Rappel : étudier le chapitre sur le boulier AVANT de venir en cours.

Qui est intéressé par

Un cours complet sur le parallélisme (spécification, programmation). Cours réalisé dans le cadre d'un projet européen (projet Papillon) ?

Je vous fournis l'ensemble du cours sur papier. J'en ai un exemplaire. Nota : le cours est en anglais. Une partie a été traduite en français (traduc sur mes pages).

Le livre conseillé

Ce français qu'on malmène, de P-V Berthier et J-P Colignon, Belin, 1991

Quelques exemples extraits du livre

• "Son patron et son épouse sont en prison", alors que le journaliste voulait dire "Son patron et l'épouse de celui-ci"
• "Rocard avait envoyé aux ministres une lettre circulaire pour menacer ceux qui viendraient à parler de réduire leur budget. " (Le Canard enchaîné)

"Ce texte contient une amphibologie, i.e. peut être compris de deux façons. On peut comprendre :

• ou bien que Rocard menaçait d'une réduction de leur budget ceux des ministres qui viendraient à parler [...]
• ou bien que, si des ministres parlaient de réduire leur budget, Rocard les avertissait sur un ton de menace [...]
  

Pour essayer l'INCLUDES

avec l'Atelier B, un petit exemple

MACHINE
contexte
SETS
ENTITE = {truc, machin}
CONSTANTS
rr
PROPERTIES
rr = {(1|->truc), (2 |->machin)}
END

MACHINE
laMienne
VARIABLES
var
INVARIANT
var : 0..100
INITIALISATION
var :: 1..100
OPERATIONS
op(mt) =
PRE
mt : 0..100 &
(var + mt) : 0..100
THEN
var := var + mt
END
END

MACHINE
incluante(ent1, ent2)
CONSTRAINTS
ent1 : ENTITE & ent2 : ENTITE & ent1 /= ent2
SEES
contexte
INCLUDES
ent1.LaMienne, ent2.LaMienne
OPERATIONS
opAppelante (mt) =
PRE
mt : NAT
THEN
ent1.op(mt) ||
ent2.op(mt)
END
END

Typez, prouvez...

Vu à la télé le ministre André Santini, ça me rappelle

sa définition du flirt

"La main dans le machin, le machin dans la main, mais jamais le machin dans le machin".

complétons notre exemple des relations amoureuses

aDansSaMainLeMachinDe : femmes >+-> hommes &
aDansSonMachinLaMainDe : femmes >+-> hommes &
/* nous restons dans les bonnes moeurs, nous avons spécifié des fonctions partielles dans les deux sens ! */
aDansSonMachinLeMachinDe : femmes >+-> hommes

DEFINITIONS
flirteAvec == (aDansSaMainLeMachinDe \/ aDansSonMachinLaMainDe) - aDansSonMachinLeMachinDe

Retour sur les hommes et les femmes

Toujours notre (en fait un exo traité par J.R. Abrial dans The B-Book, Cambridge University Press) exo Relations familiales.

On pouvait spécifier

SETS
SEXE = {masc, fem}
VARIABLES
aPourSexe, ...
INVARIANT
&
aPourSexe : PERSONNE +-> SEXE
DEFINITIONS
hommes == aPourSexe~[{masc}];
femmes == aPourSexe~[{fem}]

"Typographie, morale et diversité"

Laurent Bloch m'informe de ses derniers textes dont un qui parle de "Typographie, morale et diversité".

Vous y retrouverez Latex ....

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

Histoire de la notation lambda de Church

Gilles Dowek nous la conte dans son livre Les métamorphoses du calcul.

La notation habituelle pour les fonctions est maladroite car elle ne distingue pas la fonction de la valeur prise par la fonction en un certain point.

"Pour distinguer ces deux notions, on écrit aujourd'hui la fonction non x * x mais x |-> x * x.
Cette notation |-> aurait été introduire vers 1930 par Nicolas Bourbaki, [...]
A la même époque, Church a introduit une notation similaire : lambda x (x * x), dans laquelle la flèche |-> est remplacée par la lettre grecque lambda (2). La petite histoire raconte que cette notation vient d'une notation antérieure utilisée par Whitehead et Russell (3) dès les années 1900, x surmonté de ^ (x * x), mais que l'imprimeur (4) de Church, ne sachant pas imprimer d'accent circonflexe sur un x, l'avait fait précéder d'un symbole qui ressemblait à un accent circonflexe, le lambda majuscule, devenu par la suite minuscule.
Alors la notation x |-> x * x s'est imposée, on continue d'utiliser la notation de Church en logique et en informatique [...]"

(1) appelée maplet
(2) remplacer le mot lambda par la lettre grecque
(3) celui qui est l'auteur de la phrase que nous vous avons répétée : "en mathématique, on ne sait de quoi on parle et si ce que l'on dit est vrai". Voir notre exposé sur le concept de modèle.
(4) comme nous avec l'éditeur de blogger !