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