Mathematical Extensions - Revision history

imported>Laurent: /* Bibliography */

2014-03-17T18:20:30Z

Bibliography

← Older revision		Revision as of 18:20, 17 March 2014
Line 372:		Line 372:
	# Extensions of the Set Theory itself through the definition of algebraic types such as lists or ordered trees using new set constructors.		# 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]]

imported>Nicolas: /* Bibliography */ linked to newer version of the document

2010-11-23T13:31:51Z

Bibliography: linked to newer version of the document

← Older revision		Revision as of 13:31, 23 November 2010
Line 366:		Line 366:

	== Bibliography ==		== 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.		* J.R. Abrial, M.Butler, M.Schmalz, S.Hallerstede, L.Voisin, [http://deploy-eprints.ecs.soton.ac.uk/216 ''Proposals for Mathematical Extensions for Event-B''], 2009.
	:This proposal consists in considering three kinds of extension:		: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 set-theoretic expressions or predicates: example extensions of this kind consist in adding the transitive closure of relations or various ordered relations.

imported>Nicolas: Added Examples for Boolean Operators

2010-10-12T13:51:06Z

Added Examples for Boolean Operators

@@ Line 346: / Line 346: @@
 * OPTION #3: Workspace scope.
 :The mathematical extensions are visible to the whole workspace.
 == Bibliography ==

imported>Nicolas: /* Example: Binary PLUS */ corrected call to WDMediator for true WD

2010-06-17T13:55:01Z

Example: Binary PLUS: corrected call to WDMediator for true WD

← Older revision		Revision as of 13:55, 17 June 2010
Line 187:		Line 187:
	public Predicate getWDPredicate(IWDMediator mediator,		public Predicate getWDPredicate(IWDMediator mediator,
	IExtendedFormula formula) {		IExtendedFormula formula) {
	return mediator.~~makeChildWDConjunction~~(~~formula~~);		return mediator.makeTrueWD();
	}		}

imported>Nicolas: /* AST requirements */ added paragraph about operator properties

2010-06-17T13:49:03Z

AST requirements: added paragraph about operator properties

← Older revision		Revision as of 13:49, 17 June 2010
Line 138:		Line 138:

	[[Image:AST_Formulae.png]]		[[Image:AST_Formulae.png]]

			==== Operator Properties API ====

			Operator properties are reified through the following interfaces and enumerated:

			[[Image:AST_OperProps.png]]

	==== Extension API ====		==== Extension API ====

imported>Nicolas: /* Example: Binary PLUS */ removed methods checkPreconditions(), toString(), isFlattenable()

2010-06-10T07:52:16Z

Example: Binary PLUS: removed methods checkPreconditions(), toString(), isFlattenable()

@@ Line 173: / Line 173: @@
+  		}
   		return resultType;
+  	}
@@ Line 187: / Line 182: @@
   			IExtendedFormula formula) {
   		return mediator.makeChildWDConjunction(formula);
+  	}

imported>Nicolas: /* User Input Summarization */ updated user input

2010-06-04T13:38:28Z

User Input Summarization: updated user input

← Older revision		Revision as of 13:38, 4 June 2010
Line 256:		Line 256:
	* '''id''':		* '''id''':
	:a String id		:a String id

			* '''group id''':
			:an identifier of a existing group a new group id

	* '''kind''' (determines both the type and the notation):		* '''kind''' (determines both the type and the notation):
	:a choice between		:a choice between
	::* ~~PREFIX_PREDICATE~~: <math>\operatorname{op}(a,b,c)</math>		::* PARENTHESIZED_PREFIX_PREDICATE: <math>\operatorname{op}(a,b,c)</math>
	::* ~~PREFIX_EXPRESSION~~: ''idem''		::* PARENTHESIZED_PREFIX_EXPRESSION: ''idem''
	::* ~~BINARY_EXPRESSION~~: <math>a ~ \lozenge ~ b</math>		::* BINARY_INFIX_EXPRESSION: <math>a ~ \lozenge ~ b</math>
	::* ~~ASSOCIATIVE_EXPRESSION~~: <math>a ~ \lozenge ~ b ~ \lozenge ~ c</math>		::* ASSOCIATIVE_INFIX_EXPRESSION: <math>a ~ \lozenge ~ b ~ \lozenge ~ c</math>
	As a first step we may restrict the choice to the above list. For all these kinds, all children are expressions.		As a first step we may restrict the choice to the above list. For all these kinds, all children are expressions.

			* '''syntax symbol''':
			:a String equal to the operator to be parsed in formulæ (for instance ''"<math>\lozenge</math>"'' or ''"myOperator"'' or ''"\u03d5"'')

	* '''keyboard''':		* '''keyboard''':
Line 270:		Line 276:
	* '''parsing''':		* '''parsing''':
	:compatibility:		:compatibility:
	:* a ~~compatibility~~ group id ~~(an existing one or a new one)~~		:* a list of operator ids of the same group, that are compatible with the defined operator
	:* a list of ~~compatibility~~ group ~~ids compatible~~ with this ~~group~~		: in particular, if the id of the defined operator is included, it means it is compatible with itself
	:* a list of other ~~extension~~ ids ~~in this compatibility~~ group ~~compatible~~ with this ~~extension~~
			:priority:
			:* a list of other operator ids of the same group with higher priority than this operator
			:* a list of other operator ids of the same group with lower priority than this operator

	:~~precedence:~~		:additionally, if a new group is defined, it shall be given
	~~:* a precedence group id (an existing one or~~ a new ~~one)~~		:* the id of another group with lower priority
	~~:* a list of precedence group ids with higher priority than this~~ group		:* the id of another group with higher priority
	:* ~~a list~~ of ~~precedence~~ group ~~ids~~ with lower priority ~~than this group~~
	:* ~~a list~~ of ~~other extension ids in this precedence~~ group with higher priority ~~than this extension~~
	~~:* a list of other extension ids in this precedence group with lower priority than this extension~~

	:As these informations have a global scope, we may think about more convenient ways to input/review them, avoiding a manual scanning of all individual extensions.		:As these informations have a global scope, we may think about more convenient ways to input/review them, avoiding a manual scanning of all individual extensions.

	* '''type rule''':		* '''type rule''':
	:* a type ~~predicate~~		:* the type of every child
	:* (for ~~EXPRESSION~~) a type ~~expression~~		:as a first step we may restrict children to all bear the same type, for instance <math>\Z</math> or <math>\pow(\alpha \cprod \beta)</math>.
			:* (for expressions) the resulting type, which may depend on the type of the children
			: for instance <math>T_1 \cprod T_2</math> where <math>T_i</math> stands for the type of the i-th child.

	* '''well-definedness''':		* '''well-definedness''':
	:a ~~choice between:~~		:as a first step we will only provide a pre-defined WD condition: 'children WD conjunction', so as long as it remains so, nothing needs to be input by the user concerning WD.
	~~:* the~~ pre-defined WD condition: 'children WD conjunction'
	~~:or~~
	~~:* a custom well-definedness predicate~~

	== Impact on other tools ==		== Impact on other tools ==

imported>Nicolas: /* Example: Binary PLUS */

2010-06-04T12:10:30Z

Example: Binary PLUS

← Older revision		Revision as of 12:10, 4 June 2010
Line 175:		Line 175:
	}		}

	public ~~void~~ checkPreconditions(Expression[] expressions,		public boolean checkPreconditions(Expression[] expressions,
	Predicate[] predicates) {		Predicate[] predicates) {
	~~Assert.isTrue(~~expressions.length >= 2);		return expressions.length >= 2 && predicates.length == 0;
	~~Assert.isTrue(~~predicates.length == 0);
	}		}

Line 219:		Line 218:
	public ExtensionKind getKind() {		public ExtensionKind getKind() {
	return ExtensionKind.BINARY_INFIX_EXPRESSION;		return ExtensionKind.BINARY_INFIX_EXPRESSION;
	}

	~~public Associativity getAssociativity() {~~
	~~return Associativity.LEFT;~~
	}		}

imported>Nicolas: /* Scope of the mathematical extensions */

2010-04-27T07:54:09Z

Scope of the mathematical extensions

← Older revision		Revision as of 07:54, 27 April 2010
Line 354:		Line 354:
	:The mathematical extensions are only visible to the components that have explicitly imported them. However, note that this visibility is propagated through the hierarchy of contexts and machines (<tt>EXTENDS</tt>, <tt>SEES</tt> and <tt>REFINES</tt> clauses).		:The mathematical extensions are only visible to the components that have explicitly imported them. However, note that this visibility is propagated through the hierarchy of contexts and machines (<tt>EXTENDS</tt>, <tt>SEES</tt> and <tt>REFINES</tt> clauses).
	:An issue has been identified. Suppose that <tt>ext1</tt> extension is visible to component <tt>C1</tt> and <tt>ext2</tt> is visible to component <tt>C2</tt>, and there is no compatibility issue between <tt>ext1</tt> and <tt>ext2</tt>. It is not excluded that an identifier declared in <tt>C1</tt> conflict with a symbol in <tt>ext2</tt>. As a consequence, a global verification is required when adding a new mathematical extension.		:An issue has been identified. Suppose that <tt>ext1</tt> extension is visible to component <tt>C1</tt> and <tt>ext2</tt> is visible to component <tt>C2</tt>, and there is no compatibility issue between <tt>ext1</tt> and <tt>ext2</tt>. It is not excluded that an identifier declared in <tt>C1</tt> conflict with a symbol in <tt>ext2</tt>. As a consequence, a global verification is required when adding a new mathematical extension.
			* OPTION #3: Workspace scope.
			:The mathematical extensions are visible to the whole workspace.

	== Bibliography ==		== Bibliography ==

imported>Nicolas: /* User Input Summarization */

2010-04-27T07:25:15Z

User Input Summarization

@@ Line 262: / Line 262: @@
 :a String id
-* '''type''':
+* '''kind''' (determines both the type and the notation):
-:either EXPRESSION or PREDICATE
+:a choice between
 * '''keyboard''':
 :a list of associations 'symbol <-> ASCII shortcut' for uncommon symbols
 * '''parsing''':