Index

Symbols | A | B | C | D | E | F | G | I | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y

Symbols

  • $\mathbin \Leftrightarrow $ (equivalence),
  • $\mathbin \Rightarrow $ (implication),
  • $\lnot $ (negation),
  • $\land $ (conjunction),
  • $\lor $ (disjunction),
  • $\mathord {\top }$ (true),
  • $\mathord {\bot }$ (false),

A

  • abstract machine,
  • abstract machine notation,
  • action,
  • addition ($+$),
  • anticipated,
  • arithmetic,
  • assignment, ,
    • become element of ($\mathrel {:\mkern 1mu\in }$),
    • become such ($\mathrel {:\mkern 1mu\mid }$),
    • deterministic ($\mathrel {:\mkern 1mu=}$),
    • non-deterministic,
  • Atelier B provers,
  • auto prover,
  • auto-tactic, ,
    • preferences, ,
  • axiom, ,
    • using a wizard to create an axiom,

B

  • become element of assignment ($\mathrel {:\mkern 1mu\in }$),
  • become such assignment ($\mathrel {:\mkern 1mu\mid }$),
  • before-after predicate, ,
  • bijection ($\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $),
  • boolean,
    • as type,
    • the operator $\mathop {\mathrm{bool}}\nolimits $,
  • Boolean,
    • as type,

C

  • cardinality ($\mathop {\mathrm{card}}\nolimits $),
  • carrier set, , ,
    • using a wizard to create a carrier set,
  • Cartesian product ($\mathbin \times $),
  • combinator,
  • comment,
  • component,
  • composition,
    • backward composition of relations ($\circ $),
    • forward composition of relations ($\mathbin ;$),
  • conjunction ($\land $),
  • consistency of a machine,
  • constant, ,
    • using a wizard to create a constant,
  • context, , ,
    • creation of,
    • dependencies,
    • synthesis,
  • convergent,

D

  • data type, ,
    • Boolean,
    • carrier set,
    • integer,
    • user defined,
  • deadlock,
  • derived,
  • discharged,
  • disjunction ($\lor $),
  • division ($\div $),
  • domain ($\mathop {\mathrm{dom}}\nolimits $),
  • domain restriction ($\mathbin \lhd $),
  • domain subtraction ($\mathbin {\lhd \mkern -14mu-}$),

E

  • Eclipse, ,
  • editor,
    • Camille text editor,
    • default editor,
    • structural editor,
  • EQL (equality of preserved variable proof obligation),
  • equality ($=$),
  • equivalence ($\mathbin \Leftrightarrow $),
  • establishment of the invariant,
  • event, , ,
    • merging events,
    • using a wizard to create an event,
  • Event-B, ,
    • explorer,
    • perspective,
  • exists ($\exists $),
  • exponentation ($\mathbin {\widehat{\enskip }}$),
  • extending,
    • a context,
    • an event,
  • extends,

F

  • false,
    • as expression ($\mathord {\mathrm{FALSE}}$),
    • as predicate ($\mathord {\bot }$),
  • fast view bar,
  • feasibility,
    • of actions,
    • of witnesses,
  • FIN (finiteness proof obligation),
  • FIS (feasibility proof obligation),
  • Font,
  • for all ($\forall $),
  • free identifiers,
  • function ($ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $, $\mathbin \rightarrow $),
  • function application,

G

  • gluing invariant, ,
  • goal,
  • GRD (guard-strengthening proof obligation),
  • guard,
    • strengthening,

I

  • identifier,
  • identity relation ($\mathop {\mathrm{id}}\nolimits $),
  • implication ($\mathbin \Rightarrow $),
  • import project,
  • initialisation, ,
  • injection ($ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $,$\mathbin \rightarrowtail $),
  • integer,
    • as set ($\mathord {\mathbb Z}$),
    • as type,
  • intersection,
    • generalized intersection ($\mathrm{inter}$),
    • intersection ($\mathbin {\mkern 1mu\cap \mkern 1mu}$),
    • quantified intersection ($\bigcap \nolimits $),
  • INV (invariant proof obligation),
  • invariant, , ,
    • using a wizard to add an invariant,
  • inverse ($\mbox{}^{-1}$),

L

  • $\mathcal{L}{$-operator,
  • lamba expression ($\lambda $),
  • live lock,

M

  • machine, ,
    • dependencies,
    • synthesis,
  • mailing list,
  • maplet ($\mapsto $),
  • mathematical notation,
  • mathematical symbols,
  • maximum ($\max $),
  • membership ($\in $),
  • merging events,
  • minimum ($\min $),
  • minus ($-$),
  • modelling,
  • modulo ($\bmod $),
  • MRG (guard-strengthening (merge) proof obligation),
  • multiplication ($\cdot $),

N

  • NAT (natural number proof obligation),
  • natural numbers ($\mathord {\mathbb N}$),
  • negation ($\lnot $),
  • notation,
    • Event-B,
    • mathematical,

O

  • oftype operator ($\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$),
  • ordinary,

P

  • pair, ,
    • as type,
  • parameter, ,
  • partition,
  • pending,
  • perspective,
    • customisation,
    • Event-B,
    • proving,
  • plus ($+$),
  • post-tactic,
    • preferences,
  • post-tactics,
  • predicate,
  • predicate logic,
  • preferences,
    • prefix,
    • profile,
    • tactics, ,
  • pretty print,
  • ProB, ,
  • product,
    • direct product of relations ($\mathbin \otimes $),
    • of integers ($\cdot $),
    • parallel product of relations ($\mathbin \| $),
  • project, , ,
    • clean,
  • projection ($\mathop {\mathrm{prj}_1}\nolimits $,$\mathop {\mathrm{prj}_2}\nolimits $),
  • proof control view,
  • proof obligation,
    • action feasibility (FIS),
    • action simulation (SIM),
    • axiom as theorem (THM),
    • equality of a preserved variable (EQL),
    • generation,
    • guard as theorem (THM),
    • guard strengthening (GRD),
    • invariant as theorem (THM),
    • invariant preservation (INV),
    • merging events (MRG),
    • well-definedness of a guard (WD),
    • well-definedness of a variant (VWD),
    • well-definedness of a witness (WWD),
    • well-definedness in an action (WD),
    • well-definedness of an axiom (WD),
    • well-definedness of an invariant (WD),
    • witness feasibility (WFIS),
  • proving, , ,
    • perspective,
    • proof obligation,
    • proof rule,
    • proof tactics,
    • provers,
    • pruning,
    • purging,
    • the proof tree,
  • purging proofs,

Q

  • quantification,
    • existential ($\exists $),
    • universal ($\forall $),
 

R

  • range ($\mathop {\mathrm{ran}}\nolimits $),
  • range restriction ($\mathbin \rhd $),
  • range subtraction ($\mathbin {\rhd \mkern -14mu-}$),
  • reasoner,
  • refinement, ,
    • data refinement,
    • horizontal,
    • superposition, ,
    • vertical,
  • refines,
  • relation,
    • backward composition ($\circ $),
    • direct product ($\mathbin \otimes $),
    • forward composition ($\circ $),
    • identity ($\mathop {\mathrm{id}}\nolimits $),
    • image,
    • inverse ($\mbox{}^{-1}$),
    • parallel product ($\mathbin \| $),
  • relation ($\mathbin \leftrightarrow $,$\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$,$\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$,$\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$),
  • relational image,
  • reminder,
  • reviewed,
  • Rodin, ,
  • Rodin problems view,

S

  • sees,
  • selected hypotheses,
  • sequent,
  • set,
    • as type,
    • cardinality ($\mathop {\mathrm{card}}\nolimits $),
    • comprehension set,
    • difference set ($\setminus $),
    • empty set ($\emptyset $),
    • finite,
    • operations,
    • partition,
    • power set ($\mathop {\mathbb P\hbox{}}\nolimits $),
    • set extension,
    • set subtraction ($\setminus $),
  • SIM (simulation proof obligation),
  • skip,
  • status of an event,
  • strengthening of a guard,
  • subset ($\subseteq ,\subset $),
  • subtraction,
    • of integers ($-$),
    • of sets ($\setminus $),
  • superposition refinement,
  • surjection ($ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $,$\mathbin \twoheadrightarrow $),
  • symbols,
  • Symbols view,

T

  • tactic combinator,
  • tactics,
    • auto-tactic, ,
    • post-tactic, ,
  • theorem, ,
  • THM (theorem proof obligation),
  • true,
    • as expression ($\mathord {\mathrm{TRUE}}$),
    • as predicate ($\mathord {\top }$),
  • type,
  • type expression,

U

  • union,
    • generalized union,
    • quantified union ($\bigcup \nolimits $),
    • union ($\mathbin {\mkern 1mu\cup \mkern 1mu}$),
 

V

  • VAR (decreasing of variant proof obligation),
  • variable, ,
    • common variable,
    • creating a variable,
  • variant,
  • view,
    • Proof Control,
    • Rodin Problems view,
    • Search Hypotheses,
    • Symbols View,
  • VWD (well-definedness of variant proof obligation),

W

  • warnings,
  • WD (well-definedness proof obligation),
  • well-definedness,
  • WFIS (witness feasibility proof obligation),
  • when,
  • where,
  • witness, , , ,
  • wizard,
    • New Axioms Wizard,
    • New Carrier Sets Wizard,
    • New Constants Wizard,
    • New Enumerated Set Wizard, ,
    • New Event Wizard,
    • New Invariants Wizard,
    • New Variable Wizard,
  • WWD (well-definedness of witness proof obligation),

X

  • xulrunner,
 

Y

  • yellow highlighting,