imported>Son |
imported>Andy |
| Line 1: |
Line 1: |
| − | {{TOCright}}
| + | == The Theory Plug-in == |
| − | For the last few years, Google has offered a fantastic opportunity for students to help out Open Source software projects in the summer while getting paid for it. It's called '''Google Summer of Code™''', and it provides free software projects a great way of attracting development effort while providing software developers who are still in university with some interesting and useful experiences. Find out more about the Summer of Code (SoC) from [http://code.google.com/soc/ their site].
| + | The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code. |
| | + | === Translation Rules=== |
| | + | Figure 1 shows the interface, and some translations rules of the mapping to Ada. |
| | | | |
| − | '''Event-B''' is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. You can know more of Event-B by reading materials available on [http://www.event-b.org/ http://www.event-b.org/] | + | <div id="fig:Translation Rules"> |
| | + | <br/> |
| | + | [[Image:TheoryCGRules.png|center||caption text]] |
| | + | <center>'''Figure 1''': Translation Rules</center> |
| | + | <br/> |
| | + | </div> |
| | | | |
| − | The '''Rodin Platform''' is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. | + | The translation rules are templates used for pattern matching. The meta-variables are defined and typed, and used in the rules. Event-B expressions and predicates are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule. |
| − | | |
| − | We would like to participate in 2009's Summer of Code.
| |
| − | | |
| − | See also [http://code.google.com/opensource/gsoc/2009/faqs.html GSoC 2009 FAQ].
| |
| − | | |
| − | == Notes on applying ==
| |
| − | | |
| − | Here are some tips on what you might want to include in your application.
| |
| − | | |
| − | * First of all: get feedback on your proposal from the community. The devel [[Mailing lists|mailing list]] is a good channel for that. Ask around and get to know some people, see if they think your project is feasible or how you should change the scope to better fit the timeline and the project. (If you are new to Open Source development, reading [http://producingoss.com/en/communications.html#you-are-what-you-write this part of "Producing OSS"] may help you find the right tone.) Talking to people before applying dramatically increases your chances of approval: it shows us that you are genuinely able to communicate your ideas, allows us to gauge your expertise level and see who might be the right mentor for you.
| |
| − | | |
| − | * Tell us about yourself. We don't know you, so it helps if you give an outline of your background and what your prior experiences are (e.g. Open Source development, using Eclipse, general software engineering experience or education). If it turns out you wouldn't be a good fit for the Rodin platform or your project idea, it's helpful for everyone involved if that can be determined before you get started. However, don't hesitate to apply just because this would be your first time working in Open Source or with Eclipse; at some point this was new for each of us.
| |
| − | | |
| − | * Make it clear that you've thought through your application. Don't use a project idea from this page verbatim. Instead, come up with your own proposal, or expand on a proposal from this page. Explore the code a little bit. Make a clear schedule to show the intermediate milestones you'll reach while progressing towards your final goal.
| |
| − | | |
| − | * Let us know why you care, what you like about formal methods in general and Event-B and the Rodin platform specifically, what things you think could be improved and how they could be improved. We like working on this project because this project makes our work more effective, and we hope you'll like it, too. Showing your motivation helps.
| |
| − | | |
| − | == Getting things done ==
| |
| − | | |
| − | Some tips on how you can get to project completion within the scheduled timeline.
| |
| − | | |
| − | * Working on the Rodin platform in the summer should be your main activity. Having a vacation for one or two weeks is fine, of course, but we want you to take the project and the time mentors put into it seriously. If you are working two other jobs this summer, that probably won't work. Realize that collaborating on software development takes time, and not just the time used to reason about and write the code. This also means that we want you to set some intermediate milestones to be able to keep track of your progress.
| |
| − | | |
| − | * Communicate. In some ways, open source software development is more about communicating than about writing code. Some part of your time will be spent writing code, but a large part of the time spent will go towards explaining the code on mailing lists, asking and answering questions on IRC and in general reasoning about proposed software changes. If you can't do this, you take the risk of not understanding the goals of our project or not being able to explain why your patch is necessary.
| |
| − | | |
| − | * We want you to work in the open, with our community. Get on the [[Mailing lists|mailing lists]], both to ask for help and to provide it to other users<!--, spend time on IRC (#deploy on irc.freenode.net) discussing your work with other developers and explaining the Rodin platform to all the new users coming in with questions-->.
| |
| − | | |
| − | * We're not going to just compare what you did at the end to what you stated you'd be doing in the beginning. We want you to put effort into the project, to think about the feature you're doing, to communicate with the community and integrate your code with the project. If you end up implementing some other cool feature or fixing some annoyance, that is great as well.
| |
| − | | |
| − | == Project Ideas ==
| |
| − | | |
| − | Here are a bunch of project ideas you might like to apply for. Of course, if you have a different idea of something in the Rodin platform that badly needs fixing or some feature you think would make a difference, go ahead and apply with it!
| |
| − | | |
| − | === Tool Support for Design Patterns ===
| |
| − | | |
| − | ==== Objective ====
| |
| − | | |
| − | ==== Expected Result ====
| |
| − | | |
| − | ==== Requirements ====
| |
| − | | |
| − | ==== Mentor ====
| |
| − | Thai Son Hoang
| |
| − | | |
| − | === Integration of External Provers ===
| |
| − | | |
| − | ==== Objective ====
| |
| − | | |
| − | ==== Expected Result ====
| |
| − | | |
| − | ==== Requirements ====
| |
| − | | |
| − | ==== Mentor ====
| |
| − | Matthias Schmalz
| |
| − | | |
| − | == Mentors ==
| |
| − | | |
| − | A list of potential mentors.
| |
| − | | |
| − | * Laurent ?
| |
| − | * Son ?
| |
| − | * ...
| |
| − | | |
| − | == Students Considering Application ==
| |
| − | | |
| − | | |
| − | == Applications Received From ==
| |
| − | | |
| − | | |
| − | == Project status ==
| |
| − | | |
| − | | |
| − | == Other GSoc Projects related to RODIN ==
| |
The Theory Plug-in
The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code.
Translation Rules
Figure 1 shows the interface, and some translations rules of the mapping to Ada.
Figure 1: Translation Rules
The translation rules are templates used for pattern matching. The meta-variables are defined and typed, and used in the rules. Event-B expressions and predicates are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule.
