The Fifth Overture Workshop - Focus On Tool Development

8th and 9th of November 2008, Braga, Portugal

This workshop was organised at the University of Minho in Braga, Portugal. The overall theme of this workshop was to exercise different aspects of developing software for the Overture open source platform on top of Eclipse. The aspects that will be covered included:

• Kernel functionality developed on top of the abstract syntax using VDM++ and with code generation to java
• User interface functionality focusing on how to develop Eclipse plug-ins
• Testing using VDMUnit and JUnit of Overture components.

Workshop Programme Saturday the 8th of November

• 9:00 - 9:10 Welcome to the 5th Overture workshop by Peter Gorm Larsen
• 9:10 - 10:00 Overall structure of the Overture tool development, SourceForge, SVN, Maven and VDMTools Java code generation by Marcel Verhoef
• 10:00 - 11:00 Exercise: Structure the simple DoSort^? example according to these priciples and generate and compile Java code for it
• 11:00 - 11:15 Coffee break
• 11:15 - 11:40 Testing in Overture: VDMUnit and JUnit by Marcel Verhoef
• 11:40 - 12:10 Revisit exercise and add testing using these principles
• 12:10 - 13:00 Introduction of the Overture kernel (scanner, parser, ast file and ASTGEN) by Marcel Verhoef
• 13:00 - 14:00 Lunch
• 14:00 - 15:00 Exercise: Add "measure" for recursive functions to all components (measure.pdf: Measure Notes)
• 15:00 - 15:20 Presentation of the existing proof support component by Miguel Ferreira
• 15:20 - 15:40 Presentation of the existing UML mapper component by Kenneth Lausdahl
• 15:40 - 16:00 Presentation of the existing JML coupling and test automation components by Peter Gorm Larsen
• 16:00 - 16:15 Coffee break
• 16:15 - 19:00 Group work: Each group will restructure the component allocated to them according to the Marven principles, add tests and check it into the SVN respository at SourceForge. Marcel Verhoef will be assisting all teams. In case a group cannot complete this task at least a migration plan will be made for the remaining tasks.
• 20:00 Workshop dinner at Centurium Restaurant

Workshop Programme Sunday the 9th of November

• 9:00 - 10:00 Introduction to the principles inside Eclipse by Christian Thillemann
• 10:00 - 11:00 Explanation about how to create Eclipse plug-ins (placement of code, adding buttons and entries to menus and update-site)
• 11:00 - 11:15 Coffee break
• 11:15 - 12:15 Exercise: Adding ones own plug-in with an extra button and an extra menu item in Eclipse
• 12:15 - 13:00 Introduction to how one can call external code from Eclipse exemplified using CORBA for VDMTools and possibly connection to VDMJ by Christian Thillemann
• 13:00 - 14:00 Lunch
• 14:00 - 18:00 Group work: Each group will restructure the component allocated to them to Eclipse for real and are able to compile, test and check in these updates. Christian Thillemann (and Marcel Verhoef) will be assiting all teams. In case a group cannot complete this task at least a migration plan will be made for the remaining tasks.
• 16:00 - 16:15 Coffee break
• 18:00 - 18:30 Workshop closure including discussions on how to move forward from here managed by Peter Gorm Larsen

Preparations for workshop participants

Prior to the workshop all participants should make sure that the following things are installed on their own laptop:

• Java JDK SE 6 (install the Java Development Kit for J2SE version 6, not just the JRE)
• Eclipse Classic 3.4.1 (http://www.eclipse.org/downloads/), do NOT install Eclipse IDE for Java Developers
• Maven 2.0.9 (http://maven.apache.org/download.html)
• Maven integration for Eclipse (http://m2eclipse.codehaus.org/)
• Subversion integration for Eclipse (http://subclipse.tigris.org/)
• Download and install the latest version of jFlex
• Download and install ASTGEN and the patched version of byaccj which can be found in the Download section on the OvertureParser page.
• Windows users need to install Cygwin (Unix tools on Win32)
• Members of the proof component team must also install HOL4 and MoscowML
• And finally, create a user account for yourselves at www.sf.net and join the Overturetool project (http://sourceforge.net/projects/overture)

Group Composition

The participants have been divided up into the following groups: (more to be added when a complete list of Minho participants are available)

• Proof component: Miguel Ferreira, Jose Oliveira, Eduardo Brito, Samuel Silva, Joey Coleman and Augusto Ribeiro
• Test automation component: Peter Gorm Larsen, Luis Barbosa, Ana Paiva, Nuno Rodrigues and Hugo Pacheco
• JML and VDM++ combination component: Helder Pereira, Miguel Vilaca, Ricardo Romano and Alcino Cunha
• VDM++ and UML component: Kenneth Lausdahl, Hans Christian Agerlund Lintrup, Barbara Vieira, Miguel Marques, José Pascoal Faria and Joao Miguel Fernandes
• TraceViewer^? component: Pedro Russo and Marcel Verhoef on the Sunday
• Interpreter integration in Eclipse: Hugo Macedo, Marco Devesas Campos, Daniel Machado and Lasse Lorentzen (this team will consider how such a perspective can be made in Eclipse and analyse what needs to be changed to VDMTools' interpreter to use that here).

Helpful references

VDMUnit is described in Chapter 9 of the Validated Designs book, see www.vdmbook.com

JUnit can be found at http://junit.org and a good "junit-by-example" introduction can be found at http://junit.sourceforge.net/ For Overture, we currently use version 3.8.1 of JUnit

A very good (and free) introductionary book on Maven is Better Builds With Maven (PDF)

The definitive reference on Maven: http://oreilly.com/catalog/9780596517335/

For SVN, check the following books: http://svnbook.red-bean.com/ (also available printed as http://oreilly.com/catalog/9780596510336/)

For developing Eclipse plug-ins, check out the excellent book http://qualityeclipse.com/

The workshop is sponsored by NOKIA, Taro Kurita privately, Shin Sahara privately and Marcel Verhoef privately.

Results of workshop

An initial version of the different subprojects for the Overture tool have been established. See subproject status here.

Accomodation possibilities

Hotels direct booking by participants (please mention Overture Workshop as the prices below are reduced) SPRU Residence: must be booked by the University (send an email to lsb@di.uminho.pt specifying dates and type of accommodation required)

Albergaria Senhora-a-Branca (****) Largo da Senhora-a-Branca nº 58 4710-443 Braga Tel: (+351) 253 269938; Fax: (+351) 253 269937 WWW: http://albergariasrabranca.pt/indiceing.html email: AlbergariaSraBranca@oninet.pt Distance to the University: 20 min (walking) Prices: Single 34.5 € , Double 45 € (breakfast and private garage included) (Now full -- JoeyColeman - 30 Sep 2008)

Hotel Lamacaes (***) Av.D.João II nº75 - Nogueiró 4715 - 313 Braga Tel: (+351) 253 603 680 / 919 668 256; Fax: (+351) 253 603 689 WWW: http://www.hotel-lamacaes.com/ Distance to the University: 5 min (walking) Prices: Single 33 € , Double 40 € (breakfast included)

SPRU Braga Estacao (University Residence) Largo da Estação do Caminho de Ferro Maximinos - 4700-023 Braga Tel: (+351) 253 206500; Fax: (+351) 253 687116 WWW: http://www.spru.pt (select Braga-Estacao) Distance to the University: 30 min (walking) or bus Prices: Single 23 € Double 30 € (no breakfast)

How to get to Braga

The nearest airport is Francisco Sá Carneiro airport of Porto (http://www.ana.pt/portal/page/portal/ANA/AEROPORTO_PORTO/)

From Porto airport:

Taxi

Taking a taxi is the simplest and the fastest way (45 min). The distance between the Oporto airport and Braga is about 50km by road. The cost of traveling from the airport to the Braga city center should be around EUR 50.00.

Metro+Train

The cheapest way: Take the metro to Oporto Railway Station "Campanhã". Line E (Violet) goes to "Estadio do Dragão". Exit at Campanhã. The metro ticket should cost you around EUR 2.00. Take a train from the Campanhã train station to Braga. The train ticket should cost you around EUR 2.00. In general the earliest train to Braga leaves from Porto-Campanhã station at 6:21; the last train leaves at 22:36. Be sure to check since timetables are different on weekends. (timetables)

From Braga Train Station to Hotels:

* To Albergaria Senhora-a-Branca.

* SPRU Univeristy Residence is right next to the station.

-- PeterGormLarsen - 13 Nov 2008