Rodin Handbook





 
Previous: Where vs. When: What’s going on? Up: User Manual for Rodin v.2.3 User Manual for Rodin v.2.3

Feedback

Index

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

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,

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 $,

C

  • cardinality ($\mathop {\mathrm{card}}\nolimits $),
  • carrier set, , ,
  • Cartesian product ($\mathbin \times $),
  • comment,
  • component,
  • composition,
    • backward composition of relations ($\circ $),
    • forward composition of relations ($\mathbin ;$),
  • conjunction ($\land $),
  • consistency of a machine,
  • 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, ,
  • equality ($=$),
  • equivalence ($\mathbin \Leftrightarrow $),
  • establishment of the invariant,
  • event, , ,
    • merging events,
  • Event-B, ,
    • editor,
    • 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,
  • for all ($\forall $),
  • free identifiers,
  • function ($ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $, $\mathbin \rightarrow $),
  • function application,

G

  • gluing invariant, ,
  • goal,
  • guard,
    • strengthening,

I

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

L

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

M

  • machine, ,
    • dependencies,
    • synthesis,
  • maplet ($\mapsto $),
  • mathematical notation,
  • maximum ($\max $),
  • membership ($\in $),
  • merging events,
  • minimum ($\min $),
  • minus ($-$),
  • modeling,
  • modulo ($\bmod $),
  • multiplication ($\cdot $),

N

  • 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,
    • customization,
    • Event-B,
    • proving,
  • plus ($+$),
  • post-tactic,
    • preferences,
  • 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 of 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 $),
  • 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,

T

  • tactics,
    • auto-tactic, ,
    • post-tactic, ,
  • theorem, ,
  • 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

  • variable, ,
    • common variable,
    • creating a variable,
  • variant,
  • view,
    • Proof Control,
    • Rodin Problems view,
    • Search Hypotheses,
    • Symbols View,
 

W

  • well-definedness,
  • 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,
 

Y

  • yellow highlighting,
 
Previous: Where vs. When: What’s going on? Up: User Manual for Rodin v.2.3  
User Manual for Rodin v.2.3 : Index