Search results
From Event-B
Jump to navigationJump to searchCreate the page "Event-B Language)" on this wiki! See also the search results found.
Page title matches
- == Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial == The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin.3 KB (351 words) - 11:30, 23 January 2014
- ...s a brief summary of documents describing Event-B's logic aka mathematical language. [http://handbook.event-b.org/current/html/mathematical_notation.html Rodin Handbook (Mathematical No1 KB (203 words) - 11:28, 23 January 2014
- This page gives a brief summary of documents describing Event-B's modeling notation. [http://handbook.event-b.org/current/html/modeling_notation.html Rodin Handbook (Modeling Notation)]410 bytes (54 words) - 08:45, 27 October 2011
- ...0, Event-B components can use extended version of the Event-B mathematical language. This change was implemented then, but there were some places where strange ...e to parse them back to a tree in memory. Conversely, the serialization of Event-B formulas need to know how to transform the tree in memory into a character4 KB (692 words) - 15:06, 20 November 2013
- ....0.0. See [[Event-B_Mathematical_Language]] for a full description of the language. [[Category:Event-B]]3 KB (469 words) - 12:38, 17 April 2009
Page text matches
- == Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial == The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin.3 KB (351 words) - 11:30, 23 January 2014
- == Event-B and Rodin Documentation Wiki == [[Event-B Language]]295 bytes (39 words) - 22:09, 4 July 2008
- ...s a brief summary of documents describing Event-B's logic aka mathematical language. [http://handbook.event-b.org/current/html/mathematical_notation.html Rodin Handbook (Mathematical No1 KB (203 words) - 11:28, 23 January 2014
- ...(some) differences between the version of Event-B described in [http://www.event-b.org/abook.html Abrial's book] and the version implemented by Rodin. One may understand from Chapter 9 that Event-B is based on naive set theory, and therefore has terms like <math>\{X | X \n1 KB (188 words) - 11:10, 25 January 2012
- ...eterizable lexical analyser''' (i.e. lexer) for the [[Event-B Mathematical Language]]. In order to be usable, [[mathematical extensions]] require that the Event-B3 KB (440 words) - 09:10, 1 March 2010
- ...0, Event-B components can use extended version of the Event-B mathematical language. This change was implemented then, but there were some places where strange ...e to parse them back to a tree in memory. Conversely, the serialization of Event-B formulas need to know how to transform the tree in memory into a character4 KB (692 words) - 15:06, 20 November 2013
- * [[Records_Extension|Records]] provide structured types for Event-B. * [[UML-B]] provides a 'UML-like' graphical front end for Event-B.5 KB (757 words) - 16:19, 13 February 2020
- The need for translating the Event-B language to the SMT-LIB language was introduced by the [http://decert.gforge.inria.fr/index.html DECERT] pro ...e translation of Event-B language into the veriT extensions of the SMT-LIB language. It comes down to running a direct syntactic translation when the formula d5 KB (797 words) - 10:29, 24 October 2011
- .... The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]). * Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to3 KB (399 words) - 11:20, 27 January 2010
- ...vide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. ...other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mat4 KB (648 words) - 14:52, 7 October 2013
- ...first necessary to introduce some equivalence and simplification rules on Event-B assignments and predicates. These rules will then help to understand the tr ...an equivalence relation on the Event-B actions, and by restriction on the Event-B assignments. Two actions are considered as being equivalent if the proof ob10 KB (1,604 words) - 09:19, 27 October 2011
- ==== Mathematical Language V2 ==== [[Changes to the Mathematical Language of Event-B]] and the corresponding [[Mathematical_Language_Evolution_Design|design]] d6 KB (915 words) - 16:57, 27 February 2014
- ...traint on event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desi There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:4 KB (609 words) - 11:37, 8 January 2010
- === Tasking Event-B for D32 === Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structur7 KB (1,009 words) - 10:59, 26 January 2011
- ...vide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. ...other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mat4 KB (642 words) - 08:33, 29 June 2012
- === Tasking Event-B === Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structur6 KB (989 words) - 10:43, 10 December 2010
- * Mathematical Language V2 (releases 1.0 and upper) : The new version of the mathematical language is supported.7 KB (963 words) - 11:30, 27 January 2010
- ...ation of code for typical real-time embedded control software from refined Event-B models. Such a feature will be an important factor in ensuring eventual dep ...roject, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems12 KB (1,818 words) - 08:31, 20 April 2012
- The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This p ...clude the sequence operator (which was present in classical B mathematical language) and the bag operator.7 KB (958 words) - 14:53, 14 June 2021
- ...vide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. ...define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug7 KB (1,095 words) - 14:40, 21 December 2010
