Rodin Handbook





 

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

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

A

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

B

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

C

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

D

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

E

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

F

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

G

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

I

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

L

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

M

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

N

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

O

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

P

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

Q

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

R

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

S

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

T

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

U

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

V

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

W

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

X

  • xulrunner, 1
 

Y

  • yellow highlighting, 1