Rodin User’s Handbook v.2.8: Index

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

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