Difference between pages "Maplet Overriding in Goal" and "Mathematical Extensions"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Billaude
 
imported>WikiSysop
(New page: = Mathematical Extension = 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-defin...)
 
Line 1: Line 1:
−
This page describes the design of a tactic requested here : [https://sourceforge.net/tracker/index.php?func=detail&aid=3306228&group_id=108850&atid=651672 Feature Request #3306228]
+
= Mathematical Extension =
  
−
= Objective =
+
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
 +
including inductive data types.  Users will be able to define operators of
 +
polymorphic type as well as parameterised predicate definitions.
  
−
Split every goal in the form : <math> f \ovl{\{x \mapsto y\}} \in A \to B </math> into three sub-goals :
+
Details of the proposal may be found in this report : [http://deploy-eprints.ecs.soton.ac.uk/80/]
−
:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math>
 
−
:*<math>x \in A</math>
 
−
:*<math>y \in B</math>
 
  
−
= Design Decision =
+
The proposal consists of considering three kinds of extension:
  
−
Instead of proofing the first sub-goal, it may be more easy to proof <math>f\in A\to B</math> which is a sufficient condition : <math>(f\in A\to B)\limp (\{x\} \domsub f \in A \smallsetminus \{x\} \to B)</math>.
+
# 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.
−
= Implementation =
+
# Extensions of the Set Theory itself through the definition of algebraic types such as lists or ordered trees using new set constructors.
−
 
 
−
First, the goal is checked. Its tree structure must match the following one :
 
−
<math>\in</math>
 
−
├── <math>\ovl</math>
 
−
│   ├── f
 
−
│   └── {}
 
−
│       └──  <math>\mapsto</math>
 
−
│            ├── x
 
−
│            └── y
 
−
└── <math>\to</math>
 
−
    ├── A
 
−
    └── B
 
−
Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :
 
−
:*<math>f\in A\to B</math>
 
−
:*<math>x \in A</math>
 
−
:*<math>y \in B</math>
 
−
Else, it is split as follows :
 
−
:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math>
 
−
:*<math>x \in A</math>
 
−
:*<math>y \in B</math>
 
−
 
 
−
[[Category:Design proposal]]
 

Revision as of 22:15, 26 January 2009

Mathematical Extension

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 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 : [1]

The proposal consists of considering three kinds of extension:

  1. Extensions of set-theoretic expressions or predicates: example extensions of this kind consist of 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.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Maplet_Overriding_in_Goal&oldid=5924’