Difference between revisions of "Rodin Keyboard User Guide"

From Event-B
Jump to navigationJump to search
imported>Pascal
 
imported>Pascal
Line 17: Line 17:
  
 
=== Special Combos ===
 
=== Special Combos ===
 +
Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.
 +
   
 +
{|
 +
|ASCII || LaTeX || Math || Meaning || Unicode
 +
|-
 +
|<code>NAT</code> || \nat || <math>\nat</math> || The set of natural numbers || U+2115
 +
|-
 +
|<code>NAT1</code> || \natn || <math>\natn</math> || The set of positive natural numbers || U+2115 U+0031
 +
|-
 +
|<code>INT</code> || \intg || <math>\intg</math> || The set of integer numbers || U+2124
 +
|-
 +
|<code>POW</code> || \pow || <math>\pow</math> || The set of all subsets (power set) || U+2119
 +
|-
 +
|<code>POW1</code> || \pown || <math>\pown</math> || The set of all non-empty subsets || U+2119 U+0031
 +
|-
 +
|-
 +
|<code>(</code> || ( || ( || Left parenthesis || U+0028
 +
|-
 +
|<code>)</code> || ) || ) || Right parenthesis || U+0029
 +
|-
 +
|<code><=></code> || \leqv || <math>\leqv</math> || Logical equivalence || U+21D4
 +
|-
 +
|<code>=></code> || \limp || <math>\limp</math> || Logical implication || U+21D2
 +
|-
 +
|<code>&</code> || \land || <math>\land</math> || Logical conjunction || U+2227
 +
|-
 +
|<code>or</code> || \lor || <math>\lor</math> || Logical disjunction || U+2228
 +
|-
 +
|<code>not</code> || \lnot || <math>\lnot</math> || Not sign || U+00AC
 +
|-
 +
|<code>true</code> || \btrue || <math>\btrue</math> || True predicate || U+22A4
 +
|-
 +
|<code>false</code> || \bfalse || <math>\bfalse</math> || False predicate || U+22A5
 +
|-
 +
|<code>!</code> || \forall || <math>\forall</math> || For all || U+2200
 +
|-
 +
|<code>#</code> || \exists || <math>\exists</math> || There exists || U+2203
 +
|-
 +
|<code>,</code> || , || , || Comma || U+002C
 +
|-
 +
|<code>.</code> || \qdot || <math>\qdot</math> || Middle dot || U+00B7
 +
|-
 +
|-
 +
|<code>=</code> || = || = || Equal to || U+003D
 +
|-
 +
|<code>/=</code> || \neq || <math>\neq</math> || Not equal to || U+2260
 +
|-
 +
|<code>&lt;</code> || &lt; || &lt; || Less than || U+003C
 +
|-
 +
|<code>&lt;=</code> || \leq || <math>\leq</math> || Less than or equal to || U+2264
 +
|-
 +
|<code>&gt;</code> || &gt; || &gt; || Greater than || U+003E
 +
|-
 +
|<code>&gt;=</code> || \geq || <math>\geq</math> || Greater than or equal to || U+2265
 +
|-
 +
|<code>:</code> || \in || <math>\in</math> || Element of || U+2208
 +
|-
 +
|<code>/:</code> || \notin || <math>\notin</math> || Not an element of || U+2209
 +
|-
 +
|<code><<:</code> || \subset || <math>\subset</math> || (Proper) Subset of || U+2282
 +
|-
 +
|<code>/<<:</code> || \notsubset || <math>\not\subset</math> || Not a (proper) subset of || U+2284
 +
|-
 +
|<code><:</code> || \subseteq || <math>\subseteq</math> || Subset of or equal to || U+2286
 +
|-
 +
|<code>/<:</code> || \notsubseteq || <math>\not\subseteq</math> || Neither a subset of nor equal to || U+2288
 +
|-
 +
|-
 +
|<code><-></code> || \rel || <math>\rel</math> || Relation || U+2194
 +
|-
 +
|<code><<-></code> || \trel || <math>\trel</math> || Total relation || U+E100
 +
|-
 +
|<code><->></code> || \srel || <math>\srel</math> || Surjective relation || U+E101
 +
|-
 +
|<code><<->></code> || \strel || <math>\strel</math> || Total surjective relation || U+E102
 +
|-
 +
|<code>+-></code> || \pfun || <math>\pfun</math> || Partial function || U+21F8
 +
|-
 +
|<code>--></code> || \tfun || <math>\tfun</math> || Total function || U+2192
 +
|-
 +
|<code>>+></code> || \pinj || <math>\pinj</math> || Partial injection || U+2914
 +
|-
 +
|<code>>-></code> || \tinj || <math>\tinj</math> || Total injection || U+21A3
 +
|-
 +
|<code>+>></code> || \psur || <math>\psur</math> || Partial surjection || U+2900
 +
|-
 +
|<code>->></code> || \tsur || <math>\tsur</math> || Total surjection || U+21A0
 +
|-
 +
|<code>>->></code> || \tbij || <math>\tbij</math> || Bijection || U+2916
 +
|-
 +
|-
 +
|<code>{</code> || { || { || Left curly bracket || U+007B
 +
|-
 +
|<code>}</code> || } || } || Right curly bracket || U+007D
 +
|-
 +
|<code>|-></code> || \mapsto || <math>\mapsto</math> || Maplet || U+21A6
 +
|-
 +
|<code>,,</code>
 +
|-
 +
|<code>{}</code> || \emptyset || <math>\emptyset</math> || Empty set || U+2205
 +
|-
 +
|<code>/\</code> || \binter || <math>\binter</math> || Intersection || U+2229
 +
|-
 +
|<code>\/</code> || \bunion || <math>\bunion</math> || Union || U+222A
 +
|-
 +
|<code>\</code> || \setminus || <math>\setminus</math> || Set minus || U+2216
 +
|-
 +
|<code>**</code> || \cprod || <math>\cprod</math> || Cartesian product || U+00D7
 +
|-
 +
|-
 +
|<code>[</code> || [ || [ || Left square bracket || U+005B
 +
|-
 +
|<code>]</code> || ] || ] || Right square bracket || U+005D
 +
|-
 +
|<code><+</code> || \ovl || <math>\ovl</math> || Relation overriding || U+E103
 +
|-
 +
|<code>circ</code> || \bcomp || <math>\bcomp</math> || Backward composition || U+2218
 +
|-
 +
|<code>;</code> || \fcomp || <math>\fcomp</math> || Forward composition || U+003B
 +
|-
 +
|<code>><</code> || \dprod || <math>\dprod</math> || Direct product || U+2297
 +
|-
 +
|<code>||</code> || \pprod || <math>\pprod</math> || Parallel product || U+2225
 +
|-
 +
|<code>~</code> || \conv || ~ || Tilde operator || U+223C
 +
|-
 +
|<code><|</code> || \domres || <math>\domres</math> || Domain restriction || U+25C1
 +
|-
 +
|<code><<|</code> || \domsub || <math>\domsub</math> || Domain subtraction || U+2A64
 +
|-
 +
|<code>|></code> || \ranres || <math>\ranres</math> || Range restriction || U+25B7
 +
|-
 +
|<code>|>></code> || \ransub || <math>\ransub</math> || Range subtraction || U+2A65
 +
|-
 +
|-
 +
|<code>%</code> || \lambda || <math>\lambda</math> || Lambda || U+03BB
 +
|-
 +
|<code>INTER</code> || \Inter || <math>\Inter</math> || N-ary intersection || U+22C2
 +
|-
 +
|<code>UNION</code> || \Union || <math>\Union</math> || N-ary union || U+22C3
 +
|-
 +
|<code>|</code> || \mid || <math>\mid</math> || Such that || U+2223
 +
|-
 +
|-
 +
|<code>..</code> || \upto || <math>\upto</math> || Upto sign || U+2025
 +
|-
 +
|<code>+</code> || + || + || Addition sign || U+002B
 +
|-
 +
|<code>-</code> || - || - || Subtraction sign || U+2212
 +
|-
 +
|<code>*</code> || * || * || Multiplication sign || U+2217
 +
|-
 +
|<code>/</code> || \div || <math>\div</math> || Division sign || U+00F7
 +
|-
 +
|<code>^</code> || \expn || <math>\expn</math> || Exponentiation sign || U+005E
 +
|-
 +
|-
 +
|<code>oftype</code> || \oftype || [[Image:oftype]] || Typing operator || U+2982
 +
|-
 +
|-
 +
|<code>:=</code> || \bcmeq || <math>\bcmeq</math> || Becomes equal to || U+2254
 +
|-
 +
|<code>::</code> || \bcmin || <math>\bcmin</math> || Becomes an element of || U+003A U+2208
 +
|-
 +
|<code>:|</code> || \bcmsuch || <math>\bcmsuch</math> || Becomes such that || U+003A U+2223
 +
|}
  
 
[[Category:User documentation]]
 
[[Category:User documentation]]
 
[[Category:Work in progress]]
 
[[Category:Work in progress]]

Revision as of 18:08, 17 February 2010

Introduction

This short help page provides necessary information on the Rodin Keyboard plug-in and also on how to extend the plug-in.

Getting Started

Overview

The Rodin Keyboard plug-in creates a view (namely "RODIN Keyboard") under Event-B category.

You can open "RODIN Keyboard" view now:

  1. Go to Window/Show View/Other.
  2. Choose the "RODIN Keyboard" view from the Event-B category.

The view contains a text area which takes an ASCII input and translate it into the mathematical language (defined by extensions).

Special Combos

Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.

ASCII LaTeX Math Meaning Unicode
NAT \nat \nat The set of natural numbers U+2115
NAT1 \natn \natn The set of positive natural numbers U+2115 U+0031
INT \intg \intg The set of integer numbers U+2124
POW \pow \pow The set of all subsets (power set) U+2119
POW1 \pown \pown The set of all non-empty subsets U+2119 U+0031
( ( ( Left parenthesis U+0028
) ) ) Right parenthesis U+0029
<=> \leqv \leqv Logical equivalence U+21D4
=> \limp \limp Logical implication U+21D2
& \land \land Logical conjunction U+2227
or \lor \lor Logical disjunction U+2228
not \lnot \lnot Not sign U+00AC
true \btrue \btrue True predicate U+22A4
false \bfalse \bfalse False predicate U+22A5
! \forall \forall For all U+2200
# \exists \exists There exists U+2203
, , , Comma U+002C
. \qdot \qdot Middle dot U+00B7
= = = Equal to U+003D
/= \neq \neq Not equal to U+2260
< < < Less than U+003C
<= \leq \leq Less than or equal to U+2264
> > > Greater than U+003E
>= \geq \geq Greater than or equal to U+2265
: \in \in Element of U+2208
/: \notin \notin Not an element of U+2209
<<: \subset \subset (Proper) Subset of U+2282
/<<: \notsubset \not\subset Not a (proper) subset of U+2284
<: \subseteq \subseteq Subset of or equal to U+2286
/<: \notsubseteq \not\subseteq Neither a subset of nor equal to U+2288
<-> \rel \rel Relation U+2194
<<-> \trel \trel Total relation U+E100
<->> \srel \srel Surjective relation U+E101
<<->> \strel \strel Total surjective relation U+E102
+-> \pfun \pfun Partial function U+21F8
--> \tfun \tfun Total function U+2192
>+> \pinj \pinj Partial injection U+2914
>-> \tinj \tinj Total injection U+21A3
+>> \psur \psur Partial surjection U+2900
->> \tsur \tsur Total surjection U+21A0
>->> \tbij \tbij Bijection U+2916
{ { { Left curly bracket U+007B
} } } Right curly bracket U+007D
-> \mapsto \mapsto Maplet U+21A6
,,
{} \emptyset \emptyset Empty set U+2205
/\ \binter \binter Intersection U+2229
\/ \bunion \bunion Union U+222A
\ \setminus \setminus Set minus U+2216
** \cprod \cprod Cartesian product U+00D7
[ [ [ Left square bracket U+005B
] ] ] Right square bracket U+005D
<+ \ovl \ovl Relation overriding U+E103
circ \bcomp \bcomp Backward composition U+2218
; \fcomp \fcomp Forward composition U+003B
>< \dprod \dprod Direct product U+2297
\pprod \pprod Parallel product U+2225
~ \conv ~ Tilde operator U+223C
\domres \domres Domain restriction U+25C1
\domsub \domsub Domain subtraction U+2A64
> \ranres \ranres Range restriction U+25B7
>> \ransub \ransub Range subtraction U+2A65
% \lambda \lambda Lambda U+03BB
INTER \Inter \Inter N-ary intersection U+22C2
UNION \Union \Union N-ary union U+22C3
\mid \mid Such that U+2223
.. \upto \upto Upto sign U+2025
+ + + Addition sign U+002B
- - - Subtraction sign U+2212
* * * Multiplication sign U+2217
/ \div \div Division sign U+00F7
^ \expn \expn Exponentiation sign U+005E
oftype \oftype File:Oftype Typing operator U+2982
:= \bcmeq \bcmeq Becomes equal to U+2254
:: \bcmin \bcmin Becomes an element of U+003A U+2208
\bcmsuch \bcmsuch Becomes such that U+003A U+2223
Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Keyboard_User_Guide&oldid=7246’