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