Rodin Handbook
Handbook Home
Feedback
Email Feedback
Handbook as PDF
Handbook Hardcopy
Rodin Wiki
Rodin Download
Contact
This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a
Creative Commons Attribution 3.0 Unported License
Reference
Rodin User’s Handbook v.2.8
Rodin User’s Handbook v.2.8
3 Reference
3.1 The Rodin Platform
3.1.1 Eclipse in General
3.1.2 The Event-B Perspective
3.1.3 Customizing a perspective suitable for RODIN
3.1.4 The Event-B Editor
3.1.5 The Structural Event-B Editor
3.1.6 Wizards
3.1.7 The Proving Perspective
3.1.8 Preferences
3.2 Event-B’s modelling notation
3.2.1 About the notation that we use
3.2.2 Substitutions
3.2.3 Contexts
3.2.4 Machines
3.2.5 Well-definedness proof obligations
3.2.6 Theorems
3.2.7 Generated proof obligations
3.2.8 Visibility of identifiers
3.3 Mathematical Notation
3.3.1 Introduction
3.3.2 Predicates
3.3.3 Booleans
3.3.4 Sets
3.3.5 Relations
3.3.6 Arithmetic
3.3.7 Typing
3.3.8 Assignments
3.4 Proving
3.4.1 Sequents
3.4.2 Proof Rules
3.4.3 Proof Tactics
3.4.4 Provers
3.4.5 How to Use the Provers Effectively
3.4.6 Reasoners
3.4.7 Purging Proofs
3.4.8 Simplifying Proofs
Rodin User’s Handbook v.2.8
:
Reference