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.
lundi 12 mars 2007
mercredi 14 février 2007
Je vous adresse par courriel de nouveaux fichiers latex
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 !
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
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.
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.
mardi 13 février 2007
dimanche 11 février 2007
Lundi : toujours pas de planning de la semaine
Etonnant, n'est-ce pas aurait dit P. Desproges de Châlus.
vendredi 9 février 2007
Je vous rappelle que la semaine prochaine
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.
N'ayant pas reçu votre planning, j'ai organisé le mien.
mercredi 7 février 2007
Cahiers des charges
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
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
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.
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.
lundi 5 février 2007
jeudi 1 février 2007
La syntaxe B ASCII
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 ...
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
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>
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 ...
mardi 30 janvier 2007
Sur quelques commandes latex pour B
|-> \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
Libellés :
B,
macros latex,
package b-eves,
surjection totale,
Z
Pointeurs sur la toile
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
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
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....
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....
mercredi 24 janvier 2007
Objectif du logiciel à développer
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.
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 ?
- 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
- pour que vous me communiquiez vos questions, demandes de rdv, etc.
- pour que je réponde à vos questions
- pour conserver trace de ces échanges
Inscription à :
Articles (Atom)