Mathematical Extensions: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent m Mathematical extensions moved to Mathematical Extensions: Title case |
imported>Laurent mNo edit summary |
||
| Line 1: | Line 1: | ||
Currently the operators and basic predicates of the Event-B mathematical language supported by Rodin are fixed. | Currently the operators and basic predicates of the Event-B mathematical language supported by Rodin are fixed. | ||
We propose to extend Rodin to support user-defined data types and associated operators including | We propose to extend Rodin to support user-defined data types and associated operators including | ||
inductive data types. Users will be able to define operators of | |||
polymorphic type as well as parameterised predicate definitions. | polymorphic type as well as parameterised predicate definitions. | ||
Details of the proposal may be found in this report : [http://deploy-eprints.ecs.soton.ac.uk/80 | Details of the proposal may be found in this report : [http://deploy-eprints.ecs.soton.ac.uk/80 Proposals for Mathematical Extensions for Event-B] | ||
The proposal consists of considering three kinds of extension: | The proposal consists of considering three kinds of extension: | ||
Revision as of 15:38, 28 January 2009
Currently the operators and basic predicates of the Event-B mathematical language supported by Rodin are fixed. We propose to extend Rodin to support user-defined data types and associated operators including inductive data types. Users will be able to define operators of polymorphic type as well as parameterised predicate definitions.
Details of the proposal may be found in this report : Proposals for Mathematical Extensions for Event-B
The proposal consists of considering three kinds of extension:
- Extensions of set-theoretic expressions or predicates: example extensions of this kind consist of adding the transitive closure of relations or various ordered relations.
- Extensions of the library of theorems for predicates and operators.
- Extensions of the Set Theory itself through the definition of algebraic types such as lists or ordered trees using new set constructors.
