---
abstract: 'The Event-B method is a formal modelling approach; our interest is the final step, of generating code for concurrent programs, from Event-B. Our Tasking Event-B tool integrates Event-B to facilitate code generation. The theory plug-in allows mathematical extensions to be added to an Event-B development. When working at the implementation level we need to consider how to translate the newly added types and operators into code. In this paper, we augment the theory plug-in, by adding a Translation Rules section to the tool. This enables us to define translation rules that map Event-B formulas to code. We illustrate the approach using a small case study, where we add a theory of arrays, and specify translation rules for generating Ada code.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Edmunds
    given: Andrew
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
  - family: Maamria
    given: Issam
    honourific: ''
    lineage: ''
  - family: Silva
    given: Renato
    honourific: ''
    lineage: ''
  - family: Lovell
    given: Chris
    honourific: ''
    lineage: ''
data_type: ~
date: 2012-03
date_type: completed
datestamp: 2012-05-08 09:23:13
department: ~
dir: disk0/00/00/03/94
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 394
event_dates: 19-21 June 2012
event_location: 'Pisa, Italy'
event_title: ABZ 2012
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: ~
full_text_status: none
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
issn: ~
item_issues_comment: []
item_issues_count: ~
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2012-09-11 18:17:22
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://eprints.soton.ac.uk/336226/
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 19
series: ~
skill_areas: []
source: ~
status_changed: 2012-05-08 09:23:13
subjects:
  - ADVANCE
  - Code_generation
  - deploy_method
  - deploy_tooldev_rodinplugins
  - theory
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'Event-B code generation: type extension with theories'
type: conference_item
userid: 187
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>