Rodin Handbook
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
Queries? Please contact: Heinrich-Heine-University, Software und Programmiersprachen: To Website
Privacy Policy (Datenschutz)
 |
|
 |
Rodin User’s Handbook v.2.8 |  |
 |
|
Rodin User’s Handbook v.2.8
Rev: 16185 - Preface
- Foreword
- 1 Introduction
- 1.1 Overview
- 1.2 Further Reading
- 1.2.1 Modeling in Event-B: System and Software Engineering, J.-R. Abrial (2010)
- 1.2.2 Rodin: An Open Toolset for Modelling and Reasoning in Event-B (2009)
- 1.2.3 The B-Method, an Introduction (Steve Schneider)
- 1.2.4 Event-B Cookbook
- 1.2.5 Proofs for the Working Engineer (2008)
- 1.2.6 The Proof Obligation Generator (2005)
- 1.3 Conventions
- 1.4 Acknowledgements
- 1.5 DEPLOY
- 1.6 Creative Commons Legal Code
- 2 Tutorial
- 3 Reference
- 4 Frequently Asked Questions
- 4.1 General Questions
- 4.1.1 Where can I get help?
- 4.1.2 What is Event-B?
- 4.1.3 What is the difference between Event-B and the B method?
- 4.1.4 What is Rodin?
- 4.1.5 Where does the Rodin name come from?
- 4.1.6 Where I can download Rodin?
- 4.1.7 How to contribute and develop?
- 4.1.8 My operating system is not supported! How can I install Rodin on my platform?
- 4.2 General Tool Usage
- 4.2.1 Do I lose my proofs when I clean a project?
- 4.2.2 How do I install external plugins without using the Eclipse Update Manager?
- 4.2.3 The builder takes too long
- 4.2.4 What are the ASCII shortcuts for mathematical operators?
- 4.2.5 Pretty Print does not work on Linux
- 4.2.6 Some mathematical characters are wrong
- 4.2.7 No More Handles
- 4.2.8 Software installation fails
- 4.2.9 How do I send a bug report?
- 4.2.10 Where did the GUI window go?
- 4.2.11 Where vs. When: What’s going on?
- 4.3 Modelling
- 4.3.1 Witness for Xyz missing. Default witness generated
- 4.3.2 Identifier Xyz should not occur free in a witness
- 4.3.3 Witness Xyz must be a disappearing abstract variable or parameter in the INITIALISATION event
- 4.3.4 I’ve added a witness for Xyz but it keeps saying “Identifier Xyz has not been defined”
- 4.3.5 How can I create a new Event-B Project?
- 4.3.6 How can I remove a Event-B Project?
- 4.3.7 How can I export an Event-B Project?
- 4.3.8 How can I import a Event-B Project?
- 4.3.9 How can I change the name of a Event-B Project?
- 4.3.10 How can I create a Event-B Component?
- 4.3.11 How can I remove a Event-B Component?
- 4.3.12 In the new Rodin Editor, how can I add an element to machine?
- 4.3.13 How can I use multiple lines for a comment, predicate or expression (using the new editor)?
- 4.3.14 How can I save a Context or a Machine?
- 4.4 Proving
- 4.1 General Questions
- 5 Index
|
|
|
|
|
|