Rodin Handbook
Handbook Home
Feedback
Email Feedback
Handbook as PDF
Rodin Wiki
Rodin Download
Contact
This work is sponsored by the
Deploy Project
This work is licensed under a
Creative Commons Attribution 3.0 Unported License
Reference
User Manual for Rodin v.2.3
User Manual for Rodin v.2.3
Feedback
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 Proving Perspective
3.1.6 Auto Prover
3.1.7 Preferences
3.2 Event-B’s modeling notation
3.2.1 About the notation that we use
3.2.2 Contexts
3.2.3 Machines
3.2.4 Well-definedness proof obligations
3.2.5 Theorems
3.2.6 Generated proof obligations
3.2.7 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
User Manual for Rodin v.2.3
:
Reference