Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
2.4.1 Excursus: The specification process
While this handbook is concerned with use of the Rodin tool, it’s important to understand the specification process as well. Especially for beginners it can be daunting and unclear where to start with the model, what kind of data structures and abstractions to use, and so on.
We cover a few examples in this chapter that implicitly answer these questions, but there is no explicit set of instructions. For example, we will first model the traffic lights as booleans, and later refine them into actual colors. But how did we come up with this refinement strategy? Likewise, we decided to add the push buttons at a later refinement. In retrospect this may seem useful, but it leaves open the question on how we arrived at this structure in the first place.
Abrial has something to say about this in his book1, for which some chapters are available in the Rodin Wiki.
|
|
|
|
|
|