Projet B2Latex

La soutenance est le mardi 17 avril 06

2007-03-12T07:27:00.000-07:00

veuillez programmer une présentation orale d'ici la fin du présent mois

et m'adresser un rapport d'étape sur votre travail et sur ce qui reste à faire.

Consignes

2007-02-14T10:07:00.000-08:00

Déroulement
Planification
Consignes pour la rédaction du rapport, journal de projet, annexes
Fautes d'orthographe
Consignes de soutenance
Législation

Je vous adresse par courriel de nouveaux fichiers latex

2007-02-14T02:43:00.000-08:00

Avez-vous réussi à implanter latex ?
Il doit se trouver sous linux à l'iut, non ? Personnellement je l'utilise sous windows.

N'oubliez pas de mettre à jour votre planning au moins tous les 3 jours.

Je passe à l'iut aujourd'hui ... si pas trop tempête !

Bon courage. C'est une bonne semaine pour faire un projet !

Machines en Tex

2007-02-14T01:45:00.000-08:00

Bonjour M. Habrias,
Nous aimerions avoir d'autres exemples de documents en Latex contenant plusieurs machines afin de nous permettre de tester toutes possibilités.
Merci.

Cordialement.
Le groupe du projet b2Latex.

Cahier des charges

2007-02-13T09:05:00.000-08:00

Cahier des charges du projets :

Le planning

2007-02-13T09:02:00.000-08:00

Le planning du projet

Lundi : toujours pas de planning de la semaine

2007-02-11T23:20:00.000-08:00

Etonnant, n'est-ce pas aurait dit P. Desproges de Châlus.

Je vous rappelle que la semaine prochaine

2007-02-09T09:45:00.000-08:00

N'EST pas une semaine de vacances mais la SEULE semaine pleine disponible pour le projet !
N'ayant pas reçu votre planning, j'ai organisé le mien.

Cahiers des charges

2007-02-07T23:45:00.001-08:00

Rappel des td de Génie log

http://www.iut-nantes.univ-nantes.fr/~habrias/portailHabrias/projets_et_stages.html

exemples de cahier des charges

le DAB
http://www.atelierb.societe.com/ressources/DAB/DAB_HTML/FR/main.html

(une version papier a été présentée dans mes td)
http://www-lsr.imag.fr/B/Documents/ClearSy-CaseStudies/Index.htm

et bien sûr ce qui a été enseigné en spec1 et spec2 !

Je rappelle aussi qu'il y a eu un td sur MS project

Votre planning de la semaine prochaine

2007-02-07T23:28:00.000-08:00

Je n'ai reçu AUCUN planning. En conséquence j'ai organisé le mien.

Pour info, vous pouvez développer le logiciel par exemple en C (mais du C parfaitement commenté, voir consignes des développement de logiciels libres).

J'attends vos propositions sur l'architecture de votre logiciel (de votre "programme").

Rappel : il n'y a qu'une seule semaine à plein temps pour le projet : la semaine prochaine. Ensuite, bien peu de temps.
La "dernière" semaine sera mangée par les soutenances, ds, départ en stage (semaine "perdue" pour le projet !)

Mais vous avez certainement fait le recensement de vos plages dispos pour le projet.

J'attends votre planning

2007-02-05T09:54:00.001-08:00

J'attends :

- planning
dont répartition des tâches...

ceci avec MS project

La syntaxe B ASCII

2007-02-01T05:59:00.001-08:00

Toutes les formes syntaxiques de B ne sont pas ci-dessous. Sont présentes celles prises en compte par proB.

Logical predicates:
-------------------
P & Q conjunction
P or Q disjunction
P => Q implication
P <=> Q equivalence
not P negation
!(x).(P=>Q) universal quantification
#(x).(P&Q) existential quantification

Equality:
---------
E = F equality
E /= F disequality

Sets:
-----
{} empty set
{E} singleton set
{E,F} set enumeration
{x|P} comprehension set
POW(S) power set
POW1(S) set of non-empty subsets
FIN(S) set of all finite subsets
FIN1(S) set of all non-empty finite subsets
card(S) cardinality
S*T cartesian product
S\/T set union
S/\T set intersection
S-T set difference
E:S element of
E/:S not element of
S<:T subset of S/<:T not subset of S<<:T strict subset of S/<<:T not strict subset of union(S) generalised union over sets of sets inter(S) generalised intersection over sets of sets UNION(z).(P|E) generalised union with predicate INTER(z).(P|E) generalised intersection with predicate Numbers: -------- INTEGER set of integers NATURAL set of natural numbers NATURAL1 set of non-zero natural numbers INT set of implementable integers (MININT..MAXINT) NAT set of implementable natural numbers NAT1 set of non-zero implementable natural numbers n..m set of numbers from n to m MININT the minimum implementable integer MAXINT the maximum implementable integer m>n greater than
m=n greater than or equal
m<=n less than or equal max(S) maximum of a set of numbers min(S) minimum of a set of numbers m+n addition m-n difference m*n multiplication m/n division m**n power m mod n remainder of division PI(z).(P|E) Set product SIGMA(z).(P|E) Set summation Relations: ---------- S<->T relation
E|->F maplet
dom(r) domain of relation
ran(r) range of relation
id(S) identity relation
S<|r domain restriction S<<|r domain subtraction r|>S range restriction
r|>>S range subtraction
r~ inverse of relation
r[S] relational image
r1<+r2 right overriding r1+>r2 left overriding
r1>T partial function
S-->T total function
S+->>T partial surjection
S-->>T total surjection
S>+>T partial injection
S>->T total injection
S>+>>T partial bijection
S>->>T total bijection
%x.(P|E) lambda abstraction
f(E) function application
f(E1,...,En) is now supported (as well as f(E1|->E2))

Sequences:
----------
<> empty sequence
[E] singleton sequence
[E,F] constructed sequence
seq(S) set of sequences over Sequence
seq1(S) set of non-empty sequences over S
iseq(S) set of injective sequences
iseq1(S) set of non-empty injective sequences
perm(S) set of bijective sequences (permutations)
size(s) size of sequence
s^t concatenation
E->s prepend element
s<-E append element
rev(s) reverse of sequence
first(s) first element
last(s) last element
front(s) front of sequence (all but last element)
tail(s) tail of sequence (all but first element)
conc(S) concatenation of sequence of sequences
s/|\n take
s\|/n drop

Records:
--------
Struct(ID:S,...,ID:S) set of records with given fields and field types
rec(ID:E,...,ID:E) construct a record with given field names and values
E'ID get value of field with name ID

Trees:
------
left, right, tree, btree, ... are recognised by the parser but not yet
supported by ProB itself
Statements:
-----------
skip no operation
x:= E assignment
f(x) := E functional override
x::S choice from set
x : P choice by predicate P (constraining x)
x <-- OP(x) call operation and assign return value
G||H parallel substitution
G;H sequential composition
ANY x,... WHERE P THEN G END non deterministic choice
LET x BE x=E IN G END
VAR x,... IN G END generate local variables
PRE P THEN G END
CHOICE G OR H END
IF P THEN G END
IF P THEN G ELSE H END
IF P1 THEN G1 ELSIF P2 THEN G2 ... END
IF P1 THEN G1 ELSIF P2 THEN G2 ... ELSE Gn END
SELECT P THEN G WHEN ... WHEN Q THEN H END
SELECT P THEN G WHEN ... WHEN Q THEN H ELSE I END
CASE E OF EITHER m THEN G OR n THEN H ... END
CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END

Machine header:
---------------
MACHINE or REFINEMENT or IMPLEMENTATION

Note: machine parameters can either be SETS (if identifier is all upper-case)
or scalars (i.e., integer, boolean or SET element; if identifier is not all upper-case)

Machine sections:
-----------------
SETS
CONSTANTS
PROPERTIES
DEFINITIONS
VARIABLES
INVARIANT
INITIALISATION
OPERATIONS

Machine inclusion:
------------------
USES list of machines
INCLUDES list of machines
SEES list of machines
EXTENDS list of machines
PROMOTES list of operations
REFINES machine

Definitions:
------------
NAME1 == Expression ; NAME2(ID,...,ID) == E2 ...

Sur quelques commandes latex pour B

2007-01-30T07:13:00.000-08:00

|-> \mapsto
+-> \pfun (fonction partielle)

>< \otimes (produit direct)

|>> \rres
<<|
+->> \

>+> \pinj (injection partielle)

+->
+>  \ecrasement c'est une cde que vous trouvez en début de mes textes latex

il y a aussi
\pbij bijective partielle
\bij bijective totale

je rajoute
POW  \partition set

La surjection totale n'a pas de symbole dans B (un oubli de JR A !)
on doit la spécifier ainsi S \fun T & \land  ran(R) = T


Un message échangé avec étudiants il y a deux ans.


Avez-vous pris en compte les \newcommand que l'auteur d'un texte en latex a pu définir (ce sont des macros)

et les packages déclarés

par ex. Dans des textes portant du B, on utilise
le package b-eves où sont définis les symboles propres à Z et B

Pointeurs sur la toile

2007-01-30T07:10:00.000-08:00

Sur des logiciels de conversion
http://www.docsdunet.com/cours/faq-tex-french.html#23.5

Consignes à suivre (de manière intelligente, à adapter au projet)

http://www.iut-nantes.univ-nantes.fr/~habrias/portailHabrias/deroulementProjets.html
http://www.iut-nantes.univ-nantes.fr/~habrias/dessGledn/ConsignesRapportStage.html

Vos coordonnées SVP

2007-01-30T07:01:00.000-08:00

Suite à votre venue dans mon bureau à l'instant...je vous rappelle ce que je vous ai dit oralement :

1) me fournir vos adresses de courriel
2) préparer un planning de projet avec microsoft project
3) s'informer sur les règles de développement de logiciel libre
4) étude "toilographique" sur des logiciels à fonction équivalente
5) récupérer le style latex de B (voir site B Grenoble)
6) voir le source latex que je vais vous communiquer
7) Réfléchir à la structure de votre logiciel, au langage à utiliser
8) à son interface avec l'utilisateur

Travailler en parallèle. Pendant que l'un fait telle tâche l'autre fait....

Objectif du logiciel à développer

2007-01-24T04:30:00.000-08:00

Il s'agit de faire un logiciel qui sera "un logiciel libre" donc dont le code source sera accessible à tous.
Qui prend en entrée un texte de spécification B écrit en Latex et qui donne en sortie un texte écrit en notation B ASCII.
Le choix du langage fait partie du travail.

Ce blog pourquoi faire ?

2007-01-24T03:33:00.000-08:00

- pour vous communiquer des consignes
- pour que vous me communiquiez vos questions, demandes de rdv, etc.
- pour que je réponde à vos questions
- pour conserver trace de ces échanges