Difference between revisions of "Mathematical Extensions"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
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 define basic predicates, new operators or new algebraic types.
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 : [http://deploy-eprints.ecs.soton.ac.uk/80 Proposals for Mathematical Extensions for Event-B]
 
 
 
The proposal consists in considering three kinds of extension:
 
 
 
# Extensions of set-theoretic expressions or predicates: example extensions of this kind consist in 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.
 
 
 
  
 
== Towards a generic AST ==
 
== Towards a generic AST ==
Line 40: Line 29:
 
* <tt>org.eventb.ui</tt>
 
* <tt>org.eventb.ui</tt>
  
 +
== Bibliography ==
 +
* J.R. Abrial, M.Butler, M.Schmalz, S.Hallerstede, L.Voisin, [http://deploy-eprints.ecs.soton.ac.uk/80 ''Proposals for Mathematical Extensions for Event-B''], 2009.
 +
:This proposal consists in considering three kinds of extension:
 +
# Extensions of set-theoretic expressions or predicates: example extensions of this kind consist in 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.
  
 
[[Category:Design proposal]]
 
[[Category:Design proposal]]

Revision as of 17:05, 3 February 2010

Currently the operators and basic predicates of the Event-B mathematical language supported by Rodin are fixed. We propose to extend Rodin to define basic predicates, new operators or new algebraic types.

Towards a generic AST

The following AST parts are to become generic, or at least parameterised:

  • Lexer
  • Parser
  • Nodes ( Formula class hierarchy ): parameters needed for:
    • Type Solve (type rule needed to synthesize the type)
    • Type Check (type rule needed to verify constraints on children types)
    • WD (WD predicate)
    • PrettyPrint (tag image + notation (prefix, infix, postfix))
    • Visit Formula (getting children + visitor callback mechanism)
    • Rewrite Formula (associative formulæ have a specific flattening treatment)
  • Types (Type class hierarchy): parameters needed for:
    • Building the type expression (type rule needed)
    • PrettyPrint (set operator image)
    • getting Base / Source / Target type (type rule needed)
  • Formula Factory

Impact on other tools

Impacted plug-ins (use a factory to build formulæ):

  • org.eventb.core
  • org.eventb.core.seqprover
  • org.eventb.pp
  • org.eventb.pptrans
  • org.eventb.ui

Bibliography

This proposal consists in considering three kinds of extension:
  1. Extensions of set-theoretic expressions or predicates: example extensions of this kind consist in adding the transitive closure of relations or various ordered relations.
  2. Extensions of the library of theorems for predicates and operators.
  3. Extensions of the Set Theory itself through the definition of algebraic types such as lists or ordered trees using new set constructors.