Précédent Suivant Index

A   Eléments du langage de la méthode B

Dans cette annexe, nous récapitulons le constructions avancées de la méthode B qui seront utilisées dans ce cours. Nous indiquons dans la première colonne la notation mathématique et dans la seconde la notation ASCII utilisée dans les outils.

A.1   Opérations arithmétiques

math ASCII  
e1 + e2 e1 + e2 Addition
e1 - e2 e1 - e2 Soustraction
- e - e Moins unaire
e1 × e2 e1 * e2 Multiplication
e1 / e2 e1 / e2 Division entière
e
e2
 
1
e1 ** e2 Puissance
e1  mod  e2 e1  mod e2 Modulo

A.2   Les ensembles

A.2.1   Construction d'ensembles

math ASCII  
Ø {} Ensemble vide
N NAT Ensemble des entiers
N1 NAT1 Ensemble des entiers non nuls
{e1,...,en} {e1,...,en} Ensemble composé des éléments e1,...,en.
n1..n2 (n1..n2) ensemble composé des entiers compris entre n1 et n2
P(E) POW(E) L'ensemble des parties de E
P1(E) POW1(E) L'ensemble des parties non vides de E
F(E) FIN(E) L'ensemble des parties finies de E
E1 × E2 E1 * E2 Ensemble des couples (e1,e2) formés de e1 dans l'ensemble E1 et de e2 dans l'ensemble E2

A.2.2   Composition d'ensembles

math ASCII  
E1 È E2 E1 \/ E2 L'union des ensembles E1 et E2
E1 Ç E2 E1 /\ E2 L'intersection des ensembles E1 et E2
E1 - E2 E1 - E2 E1 auxquel on a soustrait les éléments de E2

A.2.3   Autres constructions

math ASCII  
max(E) max(E) L'entier maximal d'un ensemble fini non vide d'entiers E.
min(E) min(E) L'entier minimal d'un ensemble fini non vide d'entiers E.

A.3   Les formules

A.3.1   Formules de base

e1 et e2 représentent des expressions quelconques (entiers, ensembles, paires ...), n1 et n2 sont des expressions qui représentent des entiers.
math & ASCII
e1=e2
n1 > n2
n1 < n2
      
math ASCII
e1¹e2 e1 /= e2
n1 ³ n2 n1 >= n2
n1 £ n2 n1 <= n2

A.3.2   Formules ensemblistes

Dans le tableau suivant, e représente une expression tandis que E, E1 et E2 représentent des ensembles.

math ASCII  
e Î E e:E L'expression e est un objet de l'ensemble E
e ÏE e/:E L'expression e n'est pas un objet de l'ensemble E.
E1 Í E2 E1 <: E2 E1 est un sous-ensemble de E2.
¬ E1 Í E2 E1 /<: E2 E1 n'est pas un sous-ensemble de E2.
E1 Ì E2 E1 <<: E2 E1 est un sous-ensemble strict de E2 (différent de E2).
E1 ËE2 E1 /<<: E2 E1 n'est pas un sous-ensemble strict de E2.

A.3.3   Formules composées

Dans le tableau suivant, F, F1 et F2 représentent des formules.
math ASCII  
¬ F not(F) négation
F1 Ù F2 F1  &  F2 conjonction
F1 Ú F2 F1  or  F2 disjonction
F1 Þ F2 F1  =>  F2 implication
F1 Û F2 F1  <=>  F2 équivalence
$  var .  F #  var .  F quantification existentielle
"  var .  F !  var .  F quantification universelle

A.4   Relations et fonctions

A.4.1   Relations

E, E1 et E2 représentent des ensembles tandis que R, R1 et R2 représentent des relations.
math ASCII  
E1 « E2 E1 <-> E2 L'ensemble des relations entre éléments de E1 et de E2
    P(E1× E2)
R1;R2 R1 ; R2 Composition des relations R1 et R2
    (x,y) Î (R1;R2) Û $ z. ((x,z) Î R1 Ù (z,y) Î R2)
id(E) id(E) la relation identité sur l'ensemble E
R-1 R~ relation inverse de R
    (x,y) Î R-1 Û (y,x) Î R
E <| R E <| R la restriction de la relation R au domaine E
    (x,y) Î (E <| R) Û (x Î E Ù (x,y) Î R)
R |> E R |> E la restriction de la relation R à l'image E
    (x,y) Î (R |> E) Û ((x,y) Î RÙ y Î E )
E <<| R E <<| R l'anti-restriction de la relation R au domaine E
    (x,y) Î (E <<| R) Û (x ÏE Ù (x,y) Î R)
R |>> E R |>> E l'anti-restriction de la relation R à l'image E
    (x,y) Î (R |>> E) Û ((x,y) Î RÙ y ÏE )
R* closure(R) la fermeture transitive de R
    (x,y) Î R* Û $ (x0,...,xn). x=x0 Ù y=xn Ù " i. (xi,xi+1) Î R

Ensembles définis à partir de relations
math ASCII  
dom(R) dom(R) le domaine de la relation R
    x Î dom(R) Û ($ y. (x,y)Î R)
ran(R) ran(R) l'image de la relation R
    y Î ran(R) Û ($ x. (x,y)Î R)
R[E] R[E] l'image de l'ensemble E par la relation R
    y Î R[E] Û ($ x. x Î E Ù (x,y) Î R)

A.4.2   Fonctions

math ASCII  
E1 +-> E2 E1 +-> E2 l'ensemble des fonctions partielles de E1 dans E2
    " (x,y,z).(x|® y)Î f Ù (x |® z)Î f Þ y=z
E1 --> E2 E1 --> E2 l'ensemble des fonctions totales de E1 dans E2
    f Î E1 +-> E2 Ù " x.xÎ E1 Þ $ y. (x|® y)Î f)
E1 >+> E2 E1 >+> E2 l'ensemble des fonctions partielles injectives de E1 dans E2
    f Î E1 +-> E2 Ù (" (x,y,z).(x|® z)Î f Ù (y |® z)Î f Þ x=y)
E1 >-> E2 E1 >-> E2 l'ensemble des fonctions totales injectives de E1 dans E2
    f Î E1 --> E2 Ù (" (x,y,z).(x|® z)Î f Ù (y |® z)Î f Þ x=y)
E1 +->> E2 E1 +->> E2 l'ensemble des fonctions partielles surjectives de E1 dans E2
    f Î E1 +-> E2 Ù (" y. $ x. x|® y Î f)
E1 -->> E2 E1 -->> E2 l'ensemble des fonctions totales surjectives de E1 dans E2
    f Î E1 --> E2 Ù (" y. $ x. x|® y Î f)
E1 >->> E2 E1 >->> E2 l'ensemble des fonctions bijectives de E1 dans E2
    f Î E1 >-> E2 Ù f Î E1 -->> E2

Image d'une fonction
Si f est une fonction et e1 Î dom(f) alors f(e1) représente l'unique expression e2 telle que e1 |® e2 Î f. Si E est un ensemble alors f(E) représente l'image de E par la relation f, c'est-à-dire l'ensemble des y pour lesquels il existe x tel que x |® y Î f ou encore l'ensemble des f(x) pour xÎ E È dom(f).

A.4.3   Séquences

Dans le tableau suivant, s1 et s2 représentent des séquences, e, e1,...,en des expressions quelconques.
math ASCII  
seq(E) seq(E) L'ensemble des séquences finies d'objets de E
[] <> la séquence vide
[e] [e] la séquence réduite à un élément e
[e1,...,en] [e1,...,en] la séquence formée des n éléments e1,...,en
s1 ^ s2 s1 ^ s2 La concaténation des séquences s1 et s2
e ® s e -> s L'ajout de e au début de la séquence s
s ¬ e s <- e L'ajout de e à la fin de la séquence s
first(s) first(s) le premier élément de la séquence non-vide s
tail(s) tail(s) la séquence non-vide s privée de son premier élément
size(s) size(s) la taille de la séquence s

Chaînes de caractères
Les constantes correspondant à des chaînes de caractères sont écrites entre guillemets comme "Hello".

Précédent Suivant Index