Méthode B/Notation textuelle

Bien pratique pour les échanges sur Internet et pour saisir une machine B avec un clavier de monsieur tout le monde !

Logique

Code	Libellé	Notation Mathématique
P & Q	Conjonction	$P\land Q$
P or Q	Disjonction	$P\vee Q$
P => Q	Implication	$P\Rightarrow Q$
P <=> Q	Equivalence	$P\Leftrightarrow Q$
not(P)	Négation	$\neg P$
!(x).(P=>Q)	Quantification universelle	$\forall (x)\cdot (P\Rightarrow Q)$
#(x).(P)	Quantification existentielle	$\exists (x)\cdot (P)$

Comparaison

Code	Libellé	Notation Mathématique
E = F	Egalité	$E=F$
E /= F	Inégalité	$E\neq F$
M <= N	Inférieur ou égal	$M\leq N$
M < N	Strictement inférieur	$M<N$
M >= N	Supérieur ou égal	$M\geq N$
M > N	Strictement supérieur	$M>N$

Prédicats sur les ensembles

Code Libellé
E : S Appartenance
E /: S N'appartient pas
S <: T Sous-ensemble (inclusion)
S /<: T non inclus
S <<: T sous ensemble strict ⊂

Ensembles

Code Libellé
E |-> F Couple
S * T Produit cartésien
POW (S) Ensemble des parties de S
S \/ T Union ∪
S /\ T Intersection ∩
S - T Différence
{} Ensemble vide

Nombres

Code Libellé
NAT Les nombres naturels implantables
NAT1 Les nombres naturels implantables non nuls
card (S) Cardinal de S

Relations

Code Libellé
S <-> T Relations quelconques
dom (r) Domaine de r
ran (r) Codomaine de r
id (r) Identité de r
S <| r Restriction de domaine
S <<| r Soustraction de domaine
r |> T Restriction de codomaine
r ~ Relation inverse de r
r [S] Image de S par r (on dit aussi image relationnelle)
r1 <+ r2 Ecrasement de r1 par r2

Fonctions

Code Libellé
S +-> T ensemble des Fonctions partielles de S vers T
S --> T ensemble des Fonctions totales de S vers T
S >+> T ensemble des Injections
S >-> T ensemble des Injections totales
S +->> T ensemble des Surjections
S -->> T ensemble des Surjections totales
S >->> T ensemble des Bijections
f(E) Application de fonction

Liste

Code Libellé
<> Suite vide
seq (S) Ensemble des Suites de S
iseq (S) Ensemble des Suites injectives
j ^ k Concaténation
E -> J Ajout en début
J <- E Ajout en fin
[E] Suite singleton
size (J) Taille de la suite J
first (J) Premier élément de la suite J
last (J) Dernier élément de la suite J

Substitutions

Code Libellé
x := E Substitution simple
x,y := E,F Substitution multiple
G;H Séquence
skip Skip
x :: S Choix indéterministe de x parmi les éléments de S
x :(P) Choix par prédicat