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 !

Les relations familiales sur l'Atelier B

J'ai proposé aux étudiants d'utiliser l'Atelier B. Un (au moins, ouf ! je n'ai pas perdu mon temps) a entré la spec et ses définitions. Il a ajouté l'initialisation. Il a pu "passer le type check". Bien. Mais l'Atelier n'a pu prouver l'initialisation.
Lecture de l'obligation de preuve (Proof Obligation, PO) :
Invariant & Initialisation => {} <: PERSONNE
L'Atelier B écrit même l'invariant et l'initialisation. Partie de l'invariant on trouve que PERSONNE est un ensemble non vide et fini. Il dit tout !

Où est l'erreur ?

SETS
PERSONNE
...
hommes <: PERSONNE &
femmes <: PERSONNE &
hommes \/ femmes = PERSONNE &
hommes /\ femmes = {}

Or dans l'initialisation, on trouve :
hommes := {} || femmes := {}
ce qui fait que
hommes \/ femmes = {}
et que PERSONNE = {}

Mais l'Atelier B connaît la définition des SETS (ensembles finis et NON VIDES)

Il ne peut prouver que PERSONNE est à la fois VIDE et NON VIDE.

Ce n'est pas négociable !

Alors monsieur, on fait quoi ?

SETS
PERSONNE
...
humains <: PERSONNE &
hommes <: PERSONNE &
hommes <: humains &
femmes <: PERSONNE &
femmes <: humains &
hommes \/ femmes = humains &
hommes /\ femmes = {}

Automates et nouvelle pédagogie

"On reproche traditionnellement au machinisme :

1. de substituer des automates à des êtres conscients qui deviennent superflus ;
2. de faire servir ces automates par des êtres conscients ;
3. de transformer à la longue ces derniers en automates."

Marsal, in Lalande, Vocabulaire de la philosophie, PUF
cité par Stella Baruk, Echec et maths, Seuil

"... et seize et seize, qu'est-ce qu'ils font ?

Ils ne font rien seize et seize
et surtout pas trente-deux
de toute façon..."

Jacques Prévert

Écoutez les poètes si vous voulez spécifier correctement !

Puisqu'il faut le répéter ...

Quand vous me fournissez un travail à faire chez soi,
il faut identifier ce travail.

Fournissez les informations suivantes :

Nom du module (ex : Spec1)
Travail demandé le ......................
Rédigé par ............(nom, prénom)
Groupe ........ (n° groupe)
Le .........................
bien visibles en haut de la première page.
Paginez (n/n)
Sur chaque feuille, répéter une identification minimale.

J'ai actuellement un tas de feuilles non identifiées ou dont le n° de groupe de l'étudiant n'est pas indiqué.
Je vais les mettre sur une table lors des td et du cours. ....


Rappel de rappel de rappel :

Quand je demande en début de TD, "où en êtes-vous ?", la réponse doit se trouver en début de votre dossier de TD où vous avez noté
TD n° .......
Séance du ................, questions traitées :........................

Ce qui fait partie de la fameuse traçabilité.

Le fisc égare les données de 25 millions de contribuables

UK : Le fisc égare les données de 25 millions de contribuables
Journal du Net (21/11/2007)
L'administration fiscale britannique a égaré des données personnelles concernant la moitié de la population a reconnu mardi 21 novembre le ministre des Finances, Alistair Darling. Deux disques contenant des informations relatives à 25 millions de personnes ont disparu après avoir été confiés à la société néerlandaise de messagerie TNT NV, avec laquelle opère l'administration fiscale. Une enquête de police est en cours, mais rien n'indique pour l'heure qu'une quelconque infraction ait été commise, a-t-il souligné. Alistair Darling a jugé qu'il s'agissait d'une "erreur grave" de la part de l'administration fiscale, dont le président Paul Gray, a dû démissionner. Il ne s'agit pas de la première perte de données de cette administration.

De la fiabilité de la sous-traitance des données immatérielles ...

Le rasoir d'Occam, son histoire

Extrait de http://logictutorial.com/occam.html

Formulations of Occam's Razor:

by Russell Johnston, Victoria, BC, Canada

Occam's Razor/The Principle of Simplicity, or something like it, has been stated in more than one way.

Citing those with the most definite historical provenance first:

1a) “We may assume the superiority ceteris paribus of the demonstration which derives from fewer postulates or hypotheses.” - Aristotle, Posterior Analytics, transl. McKeon, [1963, p. 150]. [http://plato.stanford.edu/entries/simplicity/]
(As we will discuss, this may be only a principle of logic or etiquette for proofs, however, and not the more modern principle.)

1b)"the more perfect a nature is the fewer means it requires for its operation" – Aristotle

2) "Pluralitas non est ponenda sine neccesitate" or "plurality should not be posited without necessity." (a quote from Book II of Occam's Commentary on the Sentences of Peter Abelard) [http://skepdic.com/occam.html]

3) “If a thing can be done adequately by means of one, it is superfluous to do it by means of several; for we observe that nature does not employ two instruments where one suffices.” - Aquinas, T. (1945) Basic Writings of St. Thomas Aquinas, trans. A.C. Pegis, New York: Random House, p. 129.

4) “One should not increase, beyond what is necessary, the number of entities required to explain anything.” which dates from 1639, from John Ponce of Cork. [http://en.wikipedia.org/wiki/Occams_Razor]

5) “Nature does not multiply things unnecessarily; that she makes use of the easiest and simplest means for producing her effects; that she does nothing in vain, and the like” - Galileo, while comparing the Ptolemaic and Copernican theories of solar system dynamics. Galileo, G. Dialogue Concerning the Two Chief World Systems, translated by Drake (1962), Berkeley, p. 397.

6a) “Rule I: We are to admit no more causes of natural things than such as are both true and sufficient to explain their appearances.” - Newton's first of three ‘Rules of Reasoning in Philosophy’ (philosophy then included the sciences), Book III of Principia Mathematica.

As well as:

6b) “Nature is pleased with simplicity, and affects not the pomp of superfluous causes” - Newton, I. (1964) The Mathematical Principles of Natural Philosophy, New York: Citadel Press, p. 398). []
(6a is admirably specific, but seems more a truth of logic than a predictive principle when compared to 6b.)

7) “[T]he grand aim of all science…is to cover the greatest possible number of empirical facts by logical deductions from the smallest possible number of hypotheses or axioms.” - Albert Einstein [Nash, L. (1963) The Nature of the Natural Sciences, Boston: Little, Brown.].

Finally, perhaps the two most common or popular formulations of the Principle:

8) “Entia non sunt multiplicanda praeter necessitatem”, or "Entities should not be multiplied beyond necessity" (probably the most common formulation.)

9) “Of two equivalent theories or explanations, all other things being equal the simpler one is to be preferred.” - this is a common formulation, but also quite possibly the most ambiguous, which is to say least specific or informative.

Constats, contraintes, invariant

Prenons cette phrase en langage naturel : "Certains a sont b"

Supposons que :

SETS
TRUC
VARIABLES
a, b
INVARIANT
a <: TRUC & b <: TRUC

"Certains a sont b" peut se lire comme

• un fait : on constate que certains a sont b. Cela ne veut pas dire qu'il est obligatoire que certains a soient b, qu'ils le seront tout le temps, qu'il l'ont été dans le passé. On peut écrire que l'on constate que # x . x : a & x :b, il existe au moins un a qui est aussi un b. Comme on a écrit "certains", on peut même écrire # s. s <:a & card(s) >1 & s <: b, ce qui exprimer qu'il y a plus d'un a qui est b.

Mais on ne mettra pas ces prédicats dans l'INVARIANT car il ne s'agit que d'un constat et non d'une loi, d'une obligation, d'une contrainte.
Bien sûr, notre invariant actuel permet tout à fait que #1 x . x : a & x :b

• une contrainte, une obligation, une loi : il faut que certains a soient b. Par exemple, il faut qu'un Français soit chef de l'Etat à tout moment. La Constitution prévoit cela. Si un Pdt de la République meurt en exercice, il est immédiatement remplacé par le Pdt du Sénat (en termes de B, une seule opération avec deux substitutions parallèles).

Dans ce cas, on mettra nos prédicats dans l'invariant.

Ce qu'on vient de dire pour le "il existe" est aussi valable pour le "pour tous".


Vous avez bien compris ?

Alors vous avez compris que si

r1 = A -->B &
r2 = A <-->B

alors r1 <: r2 que si r1 = A +-> B &
r2 = A -->B

alors r2 <: r1 L'ensemble de toutes les fonctions totales de A vers B est inclus dans l'ensemble de toutes les fonctions partielles de B vers A. J'ai pu avoir hier constaté que tout A était lié à un et un seul B, sans pour cela avoir eu une loi obligeant tous les A à être liés à un et un seul B. J'ai alors spécifié dans mon invariant une fonction partielle (et non une fonction totale). Quand on fait l'INITIALISATION en B, on donne une valeur aux variables. On peut très bien donner une fonction totale pour initialiser une variable dont l'invariant dit que ce doit être une fonction partielle.
De le même façon, si j'ai déclaré :

SETS
ETUDIANT
VARIABLES
fumistes, mesEtudiants
INVARIANT
fumistes <: ETUDIANT &
mesEtudiants <: ETUDIANTS &

Je peux initialiser fumistes et mesEtudiants par le même sous-ensemble d'ETUDIANT, dont l'ensemble vide. MAIS mon invariant ne dit pas que tous mesEtudiants sont des fumistes.

La preuve de mon initialisation montrera que je peux au moins avoir une instanciation de mes variables qui respecte l'invariant. Que j'ai au moins un MODELE. Mais j'espère bien que jamais cela ne se réalisera .

Lire aussi sur un sujet proche

Pour savoir la différence entre Cercles d'Euler et Diagrammes de Venn

consultez mes transparents ici, voyez bien les trois lectures de quelques fumistes ne sont pas des imbéciles

Voyez bien aussi l'interprétation aristotélicienne où l'existence (il existe au moins un) est liée de manière indissoluble à l'universalité (tous)

Les profs, les bons profs, les chauves et les notes

Soit le raisonnement suivant :

1. Les profs qui donnent de bonnes notes sont des bons profs
2. Les chauves ne donnent pas de bonnes notes
3. Donc les chauves ne sont pas de bons profs

Utilisez un diagramme de Venn pour analyser ce raisonnement.

Avec un diagramme de Venn, vous représenter toutes les intersections possibles et vous rayez les zones qui ne répondent pas à vos énoncés.

Attention ! on ne peut guère utiliser la notation graphique dès que l'on a plus de 3 patates !

Lire le cours sur la logique.

Les profs, les fumistes et les chauves

Euler est un grand bonhomme. Vous avez entendu parler des graphes eulériens (c'est quoi ?). On considère que c'est l'inventeur de la théorie des graphes. Et les informaticiens aiment bien les graphes (voir cours de maths pour l'info).
Dans ses lettres à une princesse d'Allemagne, il a proposé ce qu'on a appelé les diagrammes d'Euler que l'on confondra plus tard à tord avec les diagrammes de Venn (un logicien).

En utilisant les diagrammes d'Euler, vérifiez les argument suivants

• Tous les profs sont des fumistes
• Certains fumistes sont chauves
• Donc certains profs sont chauves

• Tous les profs sont des fumistes
• Tous les fumistes sont chauves
• Donc certains profs sont chauves

• Dudule est un fumiste
• Quelques fumistes sont chauves
• Donc Dudule est un fumiste.

• Tous les profs sont chauves
• Tous les chauves sont fumistes
• Donc tous les profs sont fumistes.

Considérant
SETS
PERSONNE
VARIABLES
profs, fumistes, chauves
INVARIANT
profs <: PERSONNE & fumistes <: PERSONNE & chauves <: PERSONNE

Ecrivez chacune des phrases ci-dessus en notation ensembliste.

Vous disposez un chapitre sur la logique et la preuve dans le poly.

Ce que j'ai fait lors du 3ième cours

• un axiome de plus, celui du IF THEN ELSE et la représentation graphique du flot de contrôle avec un graphe et un ordino respectant la norme Afnor (voir autres exemples dans le poly)
• expliqué ce qu'est une architecture physique, logicielle
• posé la problématique de la composition
• traité du SEES et de l'INCLUDES avec l'exemple d'un gestionnaire de ressources avec récupération. Dans le poly il y a un chapitre à étudier sur la composition avec un petit exemple : la lampe.
• j'ai ramassé l'exo sur Qui que saille ... (fin de l'exo commencé en cours)

Le corrigé : il est dans le polycopié ! Il faut l'étudier.

Prochain cours : il va porter sur le raffinage. Il faut lire avant le chapitre sur le boulier. J'apporterai deux bouliers : un russe et un japonais.

Revoir votre cours sur la représentation des nombres. Votre CM2 sur la numération.

Le sujet du DS de Spec1

ici

Le travail à faire chez soi et à fournir en entrant dans le 4ième cours

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

Ambiguïté




Mauvais typage

Nouvelle expression en français

Spécification

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

Ambiguïté

Mauvais typage

Nouvelle expression en français

Spécification

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

Ambiguïté




Mauvais typage

Nouvelle expression en français

Spécification

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

Ambiguïté



Mauvais typage

Nouvelle expression en français

Spécification

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.

Ambiguïté



Mauvais typage

Nouvelle expression en français

Spécification



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

Poly cours

Les étudiants qui n'ont pas eu le poly peuvent me contacter de toute urgence.

Le cours du 20 novembre

aura bien lieu.

Le corrigé du travail à faire chez soi sera mis sur ce bloc-notes à l'issue du cours.

Réflexions pédagogiques

de Claude Duneton, ici

Harisa, Le phare du Cap Bon

Je lis sur la boîte :

• Ingrédients : Piment rouge fort, Ail, Coriandre, Carvi, Sel
• Contents : Hot red pimentoes, Garlic, Condiments, Salt
• Zutaten : Scharfes rotes, Paprikamark, Knoblauch, Speisewürze, Saltz

Curieux ! le carvi (caraway, Kümmel) a disparu en Anglais et en Allemand, idem pour la coriandre (coriander, Koriander)

Mystère des spécifications multi-langues

Vous pensez ? alors écrivez pour savoir ce que vous pensez !

et relisez vous !

Respécifiez la fonction solde de mon exemple hôtelier

... avec une lambda

Lambda expression en B

ou comment définir une fonction

Première construction

lambda . (x : s | E)

où s est un ensemble, x une variable non libre dans s, E une expression

ce qui se définit comme l'ensemble suivant :
{x, y | (x, y) : s * t & y = E} avec
x et y des variables non libres dans s et t, y n'étant de plus pas libre dans E, s et t sont des ensembles, E une expression, avec la condition suivante : ! x . (x : s => E : t)

Exemple :

lambda x . (x : NAT | x * x)
se définit comme l'ensemble :
{x, y | (x, y) : NAT * NAT & y = x*x}

lambda x . (x : NAT | x * x) (3) dénote l'application de la fonction au nombre naturel 3, i.e. dénote 9.

Deuxième construction

lambda x . (x : s & P | E)
avec x variable non libre dans s, E une expression et P un prédicat.
se définit comme l'ensemble :
{x, y | (x, y) : s * t & P & y = E} avec
x et y des variables non libres dans s et t, y n'étant de plus pas libre dans E, s et t sont des ensembles, E une expression, avec la condition suivante : ! x . (x : s & P => E : t)

Exemple :

lambda x . (x : NAT & x : NAT - {0} | 2 x) se définit comme l'ensemble :
{x, y| (x, y) : NAT * NAT & (x : NAT - {0}) & (y = 2x)}

Pour vous entraîner à la logique

voir Tarski's world de Barwise et Etchemendy (Stanford University)

Nouveauté B4Free avec générateur de code C

B4Free
Madame, Monsieur,
Vous êtes utilisateur de l'outil B4Free
et nous vous en remercions.
Depuis que B4free est accessible à tous,
 B4Free est soumis à une
date limite d'expiration. C'est pourquoi
 nous vous annonçons que sa
durée de validité prend fin à compter
du 1er octobre 2007.
Passé ce délai, il vous sera nécessaire
 de télécharger la nouvelle
version de l'outil. La version 3.2 que
 vous allez télécharger
correspond à l'Atelier B 3.7 et inclut
 un générateur de code C.
Pour obtenir B4Free, rendez-vous sur
la page de téléchargement du
site B4Free et suivez les instructions
 pour obtenir une nouvelle
clef de licence.
              Cordialement
            
Le Service Clientèle
 de ClearSy System Engineering 

"Le procureur dont on se méfiait"

"Une autre fois, deux hommes Y et Y furent jugés pour crime sur cette île. Le plus étonnant était que le procureur lui-même était un Pur ou un Pire. Il déclara lors du procès :

• x est coupable
• X et Y ne sont pas coupables tous les deux à la fois.

Si vous aviez été membre du jury, qu'en auriez-vous pensé ? Seriez-vous parvenu à une clonclusion quant à la culpabilité de X et de Y ? Qu'auriez-vous pensé de la sincérité de ce Procureur ? "

Raymond Smullyan, Dunod

Fallait-il le dire

"Sur une petite île on jugeait un homme accusé de crime. La Cour savait que cet homme était né et avait grandi sur l'île voisine des Purs et des Pires. Les Pires mentent toujours et les Purs disent toujours la vérité. On permit à l'accusé de faire une et une seule déclaration pour sa défense. Il réfléchit un moment puis déclara :
"L'auteur de ce crime est un Pire."

Etait-ce bien raisonnable pour lui de faire cette déclaration . Aggravait-il son cas ? Ou est-ce que cela n'avait aucune importance ? "

Raymond Smullyan, Quel est le titre de ce livre, traduc. fr. Dunod

Latex sur ma machine

Suite à la demande de certains d'entre vous ...

Sur mon pc j'utilise sous Windows, XEmacs
Pour Latex j'utilise MiKTex

Un manuel d'installation en français

Je traduis mes fichiers .dvi en fichiers .ps par la commande dvips
Et je traduis mes fichiers .ps en .pdf avec le logiciel PDFCreator.

L'organisation des universités

Une specification ici


et la spec du département info ici

Rappel

Vous disposez dans le poly des TD de consignes à suivre.
1) Qui les a lues ?
2) Qui les a appliquées ?

Je ne lirai pas de travaux, dossier de td qui ne respectent pas les consignes.

Pour ceux qui l'ignorent

L'IUT de Nantes offre à ses étudiants un accès aux ordinateurs et à l'Internet dès l'ouverture de l'IUT le matin à 20 heures le soir. Le samedi jusqu'à 12 h 30.
Il y a largement assez de machines pour chacun !

Mes bloc-notes et pages sur la Toile sont ouverts 24 h/24 ! Le poly, à vous de l'ouvrir.

Ma spec n'est pas bien !

Dans le poly, j'ai écrit

SETS
FAMILLE = {truc, much, untel}

alors que partout quand je donne par exemple comme nom de SET , ETUDIANT, GROUPE, etc,
il s'agit de l'ensemble des étudiants, des groupes, etc.

Or ici, on devrait comprendre alors que truc, much, untel désignent des familles.

Or plus loin j'ai écrit des choses qui sont correctes à condition de comprendre que truc, much et untel sont des personnes.

Il n'y a rien d'incorrect formellement. Mais on doit écrire des modèles et non uniquement de la mathématique.

Si on veut parler de familles, on peut spécifier ainsi :


SETS
FAMILLE; PERSONNE
VARIABLES
familles, est_membre_de
INVARIANT
familles <: FAMILLE &
est_membre_de : PERSONNE +-> familles


ou

SETS
PERSONNE
VARIABLES
familles, maFamille
INVARIANT
familles <: POW (POW (PERSONNE)) &
maFamille : familles
/* ma famille est bien alors un ensemble de personnes */

Relations familiales

C'est un des exos de la séquence 1 des td.

Sachez que cet exo est propre à notre civilisation occidentale.

Voici une nouvelle de l'AFP toute fraiche :


AFP - Mercredi 14 novembre, 13h02

MADRAS (AFP) - Un paysan indien a épousé une chienne dans l'espoir de chasser ce qu'il croit être une malédiction depuis qu'il a lapidé il y a quinze ans deux chiens, a rapporté la presse locale.

L'homme de 34 ans, identifié sous le nom de P. Selvakumar de l'Etat méridional du Tamil Nadu, est convaincu d'être poursuivi par le mauvais sort depuis qu'il a tué les deux canidés il y a 15 ans dans sa rizière et qu'il a accroché leurs cadavres à un arbre.

A l'époque, quelques jours après son opération punitive, il éprouve des difficultés à parler, se retrouve malentendant et incapable de marcher. Les médecins n'y trouvent aucune explication scientifique, mais un astrologue assure au paysan que les esprits des chiens défunts sont revenus le hanter et lui ont jeté un sort. La malédiction ne prendra fin que si l'homme épouse une chienne, lui dit alors le diseur de bonne aventure.

Après avoir longtemps cherché "la mariée idéale", Selvakumar finit par jeter son dévolu sur une chienne bâtarde de quatre ans, Selvi, qui lui avait été présentée par un ami. Le mariage hindou a eu lieu dimanche dans un village du Tamil Nadu. Selvi était vêtue d'un sari et ornée de fleurs. Les femmes du village du district de Sivagangawas ont ensuite emmené la chienne au temple où un prêtre hindou a prononcé le mariage religieux.

D'après la presse locale, Selvi a quand même tenté de s'échapper avant d'être rattrapée et ramenée dans les bras de son "mari".

"Le chien sert juste à éloigner la malédiction. Après cela, Selvakumar prévoit de se trouver une véritable épouse", a promis l'un de ses amis.

Attention au discours !

Voici un exemple que vous connaissez peut-être. (voir les livres de Raymond Smullyan)

3 hommes vont dans un hôtel. Le réceptionniste annonce la chambre à 30€.

Donc chacun donne 10€.

Un peu plus tard, le réceptionniste réalise que la chambre est en fait à 25€.

Il appelle le groom et l'envoie avec les 5€ chez les gars qui ont loué la chambre.

En route, le groom se demande comment il va partager les 5 € en 3.

Il décide de donner à chaque gars 1€ et garde 2€ pour lui.

Donc chacun des 3 gars a payé 9€ pour la chambre ; cela fait donc un total de 27€.

Ajoutons à ces 27€ les 2€ gardés par le groom ; cela fait 29€.

Où est l'autre euro ?


Où est le piège dans le discours ?

Modélisez par un graphe en étiquettant les arcs par le montant échangé. Pour chaque noeud, donnez le montant du flux d'entrée, celui du flux de sortie et le delta.

Il faut que je plante un reine-claude dorée

J'ai planté un mirabelle de Nancy, mais d'après la spécification trouvée dans mon livre "Savoir tout faire au jardin", il lui faut un compagnon pour qu'ils fassent des petits.

aPourNom : 1..7 >->> VARIETE_PRUNIER &
estPollinisePar : 1..7 <--> 1..7 &
estAMaturiteLe : 1..7 <--> DATE

Donnez-moi la spécification de autofertiles, ensemble des variétés autofertiles

autofertiles ==

Un bug à 10 millions d'euros

Voici ce que m'adresse mediscoop. Merci à eux.

Revue de presse du mardi 13 novembre 2007 | Envoyée à 88043 abonnés en France

« Un bug informatique coûte 10 millions d’euros à la Sécu »
Le Parisien

Le Parisien annonce en effet qu’« un logiciel déficient a provoqué des remboursements indus de soins en faveur de cliniques privées et au détriment de caisses d'assurance maladie ».
Le journal relève que « le coût pour la Sécu s'élèverait à 10 millions d'euros ».
Le quotidien explique que « ce cafouillage d'ampleur est la conséquence de la mise en place en 2001 d'un logiciel de télétransmission destiné à remplacer le format papier des demandes de remboursement ».
Le Parisien observe que « face à la complexité de la tâche, le logiciel dit des «caisses-pivots» s'est mis à totalement patauger... et les caisses ont remboursé deux, voire trois fois de suite des factures de soins qui leur étaient adressées par les cliniques ! ».
« Et le «bazar», selon l'expression d'un employé des caisses, a duré pendant des années », ajoute le journal.
Le quotidien note qu’« aujourd'hui, Pierre Fender, directeur de la répression des fraudes de la Sécurité sociale, qui a enquêté sur le sujet, se contente d'évoquer du bout des lèvres «des erreurs réelles, qui appartiennent au passé, et qui ont depuis été résolues» ».
Le Parisien remarque que « selon Pierre Fender, «la plupart des cliniques ont maintenant accepté de rembourser» ».
Le journal précise toutefois qu’« il reste au minimum 1 million d'euros d'argent non récupéré par les caisses. Et une dizaine de cliniques, qui contestent devoir rendre ces sommes, ont porté cette affaire devant les tribunaux des affaires sociales ».
Le quotidien observe par ailleurs que « la Cour des comptes travaille en ce moment sur ce sujet. La question est de savoir si certaines cliniques privées n'ont pas réussi à passer à travers les mailles du filet, en oubliant de rembourser le trop-perçu ».
Le Parisien livre un entretien avec Bernard Tepper, président de l’Union des familles laïques, qui a saisi la Cour des comptes.
Le responsable déclare que ces sommes perçues indûment par des cliniques « ont parfois été classées dans les colonnes des bénéfices », et estime que « ce sont les assurés qui seront perdants ».


Le texte est en style journalistique. Si nous trouvons des choses plus scientifiques sur ce qui s'est passé, nous vous informerons.

Si vous voulez le CD

distribué lors du Rodin Industry Day (avec exemples, plug-ins ...), me faire signe. Ou profitez du commentaire d'un des étudiants d'info 1 sur ce bloc-notes. Il vous a préparé le boulot.

La drosophile a pris la place de la droséra

dans la séquence n° 1 du poly des sujets de td.

La droséra capture...

Comme c'est bien mieux ailleurs que dans le poly qui vous a été distribué et que j'ai rédigé, vous pouvez aller voir ailleurs

"Qui est enseigné doit enseigner"

Gaston Bachelard

Certains ont ...

installé les outils B sur leur machine (voir commentaires et messages sur ce bloc-notes). Je peux leur fournir des spécifications écrites en B Ascii pour essayer les outils qu'ils ont installés. Me faire signe.

Une fois ces spécs vérifiées (syntaxe, preuve des opérations), on les mettra en ligne dans les pages B de wikipedia.

Ce que vous avez à me fournir par écrit

en entrant en cours la semaine prochaine. (travail individuel)

La spec du proverbe "Qui que saille ..."

aRenduLeTravailDemandé : inscritsInfo1 >+->> copiesFourniesALEntreeDansLAmphi

Ce que j'ai fait lors du deuxième cours

Ce matin de 8h 15 à 9 h 15

- Les axiomes des substitutions :

• skip
• préconditionnée
• gardée
• choix indéterministe

ainsi que les cas pathologiques : le crash, le miracle.
(voir l'accident du premier "vol" d'Ariane IV pour exemple de crash : non respect de précondition)
http://www.mines.inpl-nancy.fr/~tisseran/cours/qualite-logiciel/qualite_logiciel.html
Gilles Kahn, co-auteur du rapport

"Premier vol (vol 88 / 501) [modifier]

Le premier tir eut lieu le 4 juin 1996 à Kourou, mais le lanceur fut détruit après approximativement 40 secondes de vol. L'échec était dû à une erreur informatique (bogue), un programme d'un composant (un gyroscope) provenant d'Ariane 4 n'ayant pas été re-testé.^[1]

L'erreur

La conversion d'un nombre flottant de 64 bits vers un nombre entier de 16 bits dans un logiciel en Ada provoqua un dépassement de mantisse. La routine de gestion de cette erreur avait également été supprimée pour des raisons de temps d'exécution ; sur Ariane 4 on pouvait prouver que l'occurrence d'un tel dépassement était impossible compte tenu des trajectoires de vol possibles. Toutefois les trajectoires de vol envisageables avec Ariane 5, notamment en phase de décollage, diffèrent notablement de celles d'Ariane 4. Le programme du composant concerné, pourtant lui-même redondant (deux gyroscopes sont présents dans la cellule de la fusée), déclencha donc successivement deux dépassements pour finir par signaler sur les sorties du système la défaillance des systèmes gyroscopiques. De toute façon, le gyroscope étant un système critique, le calculateur de pilotage de la fusée (lui conçu spécifiquement pour Ariane 5) ne tenait pas compte de ce signal d'erreur ! Il interpréta donc les valeurs d'erreurs (probablement négatives) du deuxième gyroscope comme une information d'attitude (indiquant probablement que, brutalement, la fusée s'était mise à pointer vers le bas). La réaction du calculateur de pilotage (braquer les tuyères au maximum pour « redresser ») augmenta considérablement l'incidence du lanceur (angle entre le vecteur vitesse et l'axe du lanceur), ce qui provoqua des efforts aérodynamiques suffisants pour détruire le lanceur ^[2]. Il s'agit certainement là d'une des erreurs informatiques les plus coûteuses de l'histoire ^[3].

Le programme en question était destiné à recalibrer les gyroscopes dans le cas d'un court retard de tir (quelques minutes) pour permettre une reprise rapide du compte à rebours - par exemple en raison de variations rapides des conditions météo du site de lancement à Kourou. Ce cas de figure, envisagé initialement pour Ariane 3, était depuis longtemps exclu des procédures de tir. L'erreur en question a donc aussi été provoquée par un programme qui ne servait à rien. "

source : Wikipedia

Si vous désirez le rapport d'enquête complet, me faire signe.

- Rappel de la notation pour les relations, fonctions

- Analyse du proverbe
" Qui que saille notre jument, le poulain est notre."

J'ai spécifié le "Qui que"
le "saille"
le "notre jument"
le "est notre"
"a pour mère"
"a pour père"

J'ai tenté de faire comprendre que si on spécifiait des fonctions totales pour "a pour mère" et
"a pour père", étant donné ce que nous n'avions pas spécifié mais que vous savez : un père ne peut être son propre père et si a est père de b et b père de c, c ne peut être père de a (voir votre cours sur relations d'ordre), nous avions des ensembles infinis. Bonne occasion pour revoir votre cours de philo ou de religions comparées.

Merci merci pour cette co(q)uille qui n'en finit pas de revenir

Un étudiant m'a fait remarquer que le paragraphe 1.2.4 du poly de cours avait plusieurs erreurs.

Vous aviez tous bien sûr repéré ces erreurs manifestes.

Avant :

x= 3 & y = 1

Opération (substitution)

y := x + 2 ; x := x + 2

Après :

x = 5 & y = 3


Avant

x= 3 & y = 1

Opération (substitution)
x:= x + 2 ; y := y + x

Après

x = 5 & y = 6


Avant

x= 3 & y = 1

Opération (substitution)
y := y + x ; x := x + 2

Après

x = 5 & y = 4

J'espère ne pas avoir écrit une ...

Quand on fera du raffinage en B, on prouvera que ce que l'on a écrit au niveau abstrait (sans séquencement) est bien réalisé par l'implantation (où on a introduit le séquencement).

btoolkit

L'atelier anglais
http://www.b-core.com/btoolkit_main.html

B4free

http://www.b4free.com/installb4w.htm

Le premier manuel de référence d'Ada

J.D. Ichbiah, B. Krieg-Brückner, A. Wichmann, H.F. Ledgard, J.-C. Heliard, J.R. Abrial, J.P.G. Barnes, O. Roubine (1979). Preliminary Ada Reference Manual. ...

Un peu d'histoire ...

"

For two days, we had two speakers in the morning and three speakers in the afternoon:

-- R. Kowalski, D.A. Turner

-- D.I. Good, R. Milner, P. Martin-Löf (a last-minute replacement of D.S. Scott, who had suddenly decided not to show up)

-- E.M. Clarke, L.G. Valiant

-- J.R. Abrial, C.A.R. Hoare, E.W. Dijkstra. "

Un compte rendu de Dijkstra

Les pages d'un ancien collègue de l'IUT de Nantes

http://www.lirmm.fr/~leclere/enseignements/SpecForm/

A mes trois groupes de TD

Rappel : Vous avez à faire chez vous (ou ailleurs !) - les anglo-saxons appellent cela du homework - les questions sur le concept de modèle qui sont dans la première séquence de TD.
Copies à fournir en entrant en séance de td.

Rappel : mes pages sur la Toile

ou tapez tout simplement mon nom "sur Google". Ça marche !


Avant de venir en TD, étudiez le cours. Le TD est l'application du cours. Ce n'est pas la répétition du cours et l'écriture de corrigés au tableau.

Si vous voulez rédiger des textes avec des notations mathématiques

faites comme beaucoup d'étudiants en informatique de par le monde, utilisez Latex (prononcez latek).

Je peux vous fournir le fichier source par exemple du polycopié des td (fait en Latex) et les fontes pour B. Pour le reste, utilisez la Toile. Vous y trouverez le nécessaire. Latex, c'est gratuit. C'est construit sur Tex de Donald Knuth, bien connu des informaticiens, pour entre autres choses, sa bible des algos

Bonne fin de semaine.

Oh ! la belle faute, .. ou co (q)uille

Pas un seul n'a repéré la faute en bas de la page 1 du poly des sujets de td.

Quelle est cette faute*. ? Il suffit (?!) de savoir ce qu'est l'appartenance, l'inclusion ensembliste et le produit cartésien.

* il s'agit d'un texte mathématique mal formé

Le VAL à Roissy et la méthode B

J.L. Boulanger nous informe sur le logiciel réalisé avec la

méthode B et l'Atelier B que nous enseignons (encore !) et
utilisons.


" quelques chiffres fournis par
l'industriel

Sur la ligne L1 du VAL inauguré le 4 Avril 2007
on a 2 calculateurs, l'UCA et
le PADS (autant de PADS que de besoin - S pour Section).

Pour le PADS :
    186 440 lignes  pour le code Ada sécu
de l'AS (AS - Application de Sécurité)
    30 632 lignes pour le code Ada non-sécu
de l'AS
    nombre de PO : 62 056
    nombre de lignes B : 256 653 lignes
Pour l'UCA :
    50 085 lignes pour le code Ada sécu
de l'AS
    11 662 lignes pour le code Ada
non-sécu de l'AS
    nbre de PO : 12 811
    nombre de lignes B : 65 722 lignes

Le nombre de lignes de B effectives est moindre
que celui annoncé car il y a
prise en compte des commentaires, dont des
commentaires qui guident les
raffinements.

Une seconde ligne pour l'aéroport CdG devrait
être inauguré en Juin 2007."

Pour des photos, voici les notres ici

Monsieur, on voudrait un atelier B pour nous, chez nous

Ben, pas de pb, voir mes pages, b4free, projet Rodin etc....

Le deuxième cours

Il portera sur :

• le concept de plus faible précondition
• sur la preuve d'une opération en B
• et on spécifiera quelques opérations (vous devez avoir étudié les machines commentées qui sont sur mes pages)

Si vous avez des questions précises (vous devez rédiger ce que vous avez à me demander) , le courriel et le blog est à votre disposition. Soyons modernes intelligemment.

Servez-vous de l'Atelier B

Facile !
Merci Google. Tapez mode d'emploi atelier B et Google vous mène directo à ma page (extra : pas besoin de lire ce tout ce que j'ai rédigé pour vous)

Si vous suivez rigoureusement, ça marche. J'ai des preuves vivantes : des étudiants.

Le premier cours du 6 novembre 07

1) Ce que j'ai traité

• expression, prédicat, commande
• variables, constantes
• invariant, propriétés
• machine abstraite
• SETS (ensembles de base)
  
• initialisation, modèle
• preuve de l'initialisation
  
• opérations

Travail à faire : étudier dans le polycop la sémantique de mon opération "inscription" (le ANY WHERE)

Etudier les premiers chapitres du polycopié.

Et l'exemple commenté suivant :
ici


B sur wikipedia