Rodin Plug-ins - Revision history

imported>Richardcook: Undo revision 14486 by Richardcook (talk)

2020-02-13T16:19:41Z

Undo revision 14486 by Richardcook (talk)

← Older revision		Revision as of 16:19, 13 February 2020
Line 63:		Line 63:
	* [[Requirements Tutorial]],		* [[Requirements Tutorial]],
	* [[AnimB Flash Tutorial\|Flash Animation Tutorial]] with animB and Adobe CS3.		* [[AnimB Flash Tutorial\|Flash Animation Tutorial]] with animB and Adobe CS3.
	* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial] ~~Tesst~~		* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial]
	== Tips & Tricks ==		== Tips & Tricks ==

imported>Richardcook at 16:19, 13 February 2020

2020-02-13T16:19:22Z

← Older revision		Revision as of 16:19, 13 February 2020
Line 63:		Line 63:
	* [[Requirements Tutorial]],		* [[Requirements Tutorial]],
	* [[AnimB Flash Tutorial\|Flash Animation Tutorial]] with animB and Adobe CS3.		* [[AnimB Flash Tutorial\|Flash Animation Tutorial]] with animB and Adobe CS3.
	* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial]		* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial] Tesst
	== Tips & Tricks ==		== Tips & Tricks ==

imported>Son: /* Rodin Plug-in Documentation */

2018-11-13T14:19:48Z

Rodin Plug-in Documentation

← Older revision		Revision as of 14:19, 13 November 2018
Line 6:		Line 6:
	* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.		* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
	* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.		* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
	* [[CamilleX]] formerly XEvent-B) with support for text editors and modelling mechanisms such as ''machine inclusion''.		* [[CamilleX]] (formerly XEvent-B) with support for text editors and modelling mechanisms such as ''machine inclusion''.
	* [[Records_Extension\|Records]] provide structured types for Event-B.		* [[Records_Extension\|Records]] provide structured types for Event-B.
	* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.		* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.

imported>Son: /* Modelling */

2018-11-13T14:19:32Z

Modelling

← Older revision		Revision as of 14:19, 13 November 2018
Line 6:		Line 6:
	* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.		* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
	* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.		* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
	* [[CamilleX]] ~~CamilleX (~~formerly XEvent-B) with support for text editors and modelling mechanisms such as ''machine inclusion''.		* [[CamilleX]] formerly XEvent-B) with support for text editors and modelling mechanisms such as ''machine inclusion''.
	* [[Records_Extension\|Records]] provide structured types for Event-B.		* [[Records_Extension\|Records]] provide structured types for Event-B.
	* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.		* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.

imported>Son: /* Rodin Plug-in Documentation */

2018-11-13T14:19:19Z

Rodin Plug-in Documentation

← Older revision		Revision as of 14:19, 13 November 2018
Line 6:		Line 6:
	* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.		* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
	* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.		* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
	* [[~~XEvent-B~~]] ~~eXtended Event~~-B with support for text editors and modelling mechanisms such as ''machine inclusion''.		* [[CamilleX]] CamilleX (formerly XEvent-B) with support for text editors and modelling mechanisms such as ''machine inclusion''.
	* [[Records_Extension\|Records]] provide structured types for Event-B.		* [[Records_Extension\|Records]] provide structured types for Event-B.
	* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.		* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.

imported>Son: /* Modelling */

2017-07-21T23:18:36Z

Modelling

← Older revision		Revision as of 23:18, 21 July 2017
Line 6:		Line 6:
	* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.		* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
	* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.		* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
	* [[~~Event~~-B ~~XText Front-end~~]] ~~provides the text editor front-end for~~ Event-B ~~constructs, i.e., machines~~ and ~~contexts~~.		* [[XEvent-B]] eXtended Event-B with support for text editors and modelling mechanisms such as ''machine inclusion''.
	* [[Records_Extension\|Records]] provide structured types for Event-B.		* [[Records_Extension\|Records]] provide structured types for Event-B.
	* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.		* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.

imported>Son: /* Modelling */

2016-11-04T15:06:56Z

Modelling

← Older revision		Revision as of 15:06, 4 November 2016
Line 6:		Line 6:
	* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.		* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
	* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.		* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
			* [[Event-B XText Front-end]] provides the text editor front-end for Event-B constructs, i.e., machines and contexts.
	* [[Records_Extension\|Records]] provide structured types for Event-B.		* [[Records_Extension\|Records]] provide structured types for Event-B.
	* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.		* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.

imported>Neoser: /* Code Generation */

2015-05-28T06:39:21Z

Code Generation

← Older revision		Revision as of 06:39, 28 May 2015
Line 46:		Line 46:
	* [[Code Generation\|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.		* [[Code Generation\|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.
	* [[B2C plugin\|B2C]] translates Event-B models to C source code, which may then be compiled using external C development tools.		* [[B2C plugin\|B2C]] translates Event-B models to C source code, which may then be compiled using external C development tools.
	* [http://~~eventb-to-vhdl~~.tk/ EHDL] The plug-in enables [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6037401 VHDL code generation] from formal Event-B models automatically.		* [http://www.eb2vhdl.tk/ EHDL] The plug-in enables [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6037401 VHDL code generation] from formal Event-B models automatically.

	=== Experimental ===		=== Experimental ===

imported>Rivera: /* Code Generation */ added EventB2SQL

2015-01-06T15:56:43Z

Code Generation: added EventB2SQL

← Older revision		Revision as of 15:56, 6 January 2015
Line 42:		Line 42:
	* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.		* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
	* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.		* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.
			* [http://users.dickinson.edu/~wahlst/eventb2sql/eventb2sql.html EventB2SQL] translates Event-B machines to Java implementations that make the state of a machine persistent by storing it in a database.
	* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.		* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.
	* [[Code Generation\|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.		* [[Code Generation\|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.

imported>Rivera: /* Code Generation */

2015-01-06T12:58:30Z

Code Generation

← Older revision		Revision as of 12:58, 6 January 2015
Line 40:		Line 40:
	=== Code Generation ===		=== Code Generation ===
	* [http://poporo.uma.pt/favas/EventB2Java.html EventB2Java] generates JML-specified Java implementations of Event-B models. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.		* [http://poporo.uma.pt/favas/EventB2Java.html EventB2Java] generates JML-specified Java implementations of Event-B models. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
	* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera		* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
	* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.		* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.
	* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.		* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.