add first text about Event-B

259e2a27 · Michael Leuschel · 4184bb5a · 259e2a27
Commit 259e2a27 authored 2 years ago by Michael Leuschel
--- a/notebooks/manual/FloatsReals.ipynb
+++ b/notebooks/manual/FloatsReals.ipynb
@@ -786,7 +786,24 @@
   "cell_type": "markdown",
   "id": "cc7e1768",
   "metadata": {},
-   "source": []
+   "source": [
+    "## Event-B Theories\n",
+    "Event-B does not have support for reals or floats as basic type but one can use the theory plugin.\n",
+    "\n",
+    "[https://prob.hhu.de/w/index.php?title=Event-B_Theories]\n",
+    "\n",
+    "To be able to view reals in ProB within Rodin you need to install a recent nightly build: [https://www3.hhu.de/stups/rodin/prob1/nightly]\n",
+    "\n",
+    "You need to use one of the standard theories.\n",
+    "\n",
+    "To write your own theory you should add an axiomatic type called REAL, FLOAT or the unicode R for reals.\n",
+    "Then you have to define axiomatic operators and link them to ProB's real operators.\n",
+    "You can do this either\n",
+    "* using a theory mapping file (.ptm extension) which needs to be put into the Rodin project, see [https://prob.hhu.de/w/index.php?title=Event-B_Theories]\n",
+    "* or use the same name as the external functions above (e.g., RSQRT); in this way ProB will do the mapping automatically.\n",
+    "\n",
+    "\n"
+   ]
  }
 ],
 "metadata": {

 %% Cell type:markdown id:85001897 tags:

 # Reals and Floats in ProB

 ### Michael Leuschel

 %% Cell type:markdown id:42473a5e tags:

 ## Classical B

 In Atelier-B the following two types were added to the B language:
 * REAL
 * FLOAT

 ProB treats these keywords as synonyms for a new base type.
 The current representation in ProB are floating point numbers; but this
 will probably change in the future, at least for the REAL type.

 One can now also use literals in decimal point notation for REAL and FLOAT.

 %% Cell type:code id:cf76baf3 tags:

 ``` prob
 1.0
 ```

 %% Output

    $1.0$
    1.0

 %% Cell type:code id:941433ba tags:

 ``` prob
 1.0 : REAL & 1.0 : FLOAT
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id:6caf3504 tags:

 ### Conversion Operators
 The following conversion operators are available in classical B:
 * floor
 * ceiling
 * real

 %% Cell type:code id:8925f6fe tags:

 ``` prob
 real(2)
 ```

 %% Output

    $2.0$
    2.0

 %% Cell type:code id:bbd73954 tags:

 ``` prob
 floor(2.2)
 ```

 %% Output

    $2$
    2

 %% Cell type:code id:838ea786 tags:

 ``` prob
 ceiling(2.2)
 ```

 %% Output

    $3$
    3

 %% Cell type:code id:ee31f934 tags:

 ``` prob
 ceiling(-2.2)
 ```

 %% Output

    $-2$
    −2

 %% Cell type:markdown id:f7398e0e tags:

 ### Arithmetic Operators

 The documentation of Atelier-B is not entirely consistent according to which
 operators to use.
 In ProB you can use the standard arithmetic operators also for
 floats:

 %% Cell type:code id:65a66ec9 tags:

 ``` prob
 1.0 + 1.0
 ```

 %% Output

    $2.0$
    2.0

 %% Cell type:code id:35ce95d5 tags:

 ``` prob
 2.0 * 2.0 < 2.1
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:code id:531aa72d tags:

 ``` prob
 2.0 * 2.0 < 2.0 + 2.0
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:markdown id:9066aa50 tags:

 You can control whether to allow arithmetic operators for reals
 in ProB via the preference ```ALLOW_REALS```.
 By default reals are allowed for classical B and disallowed for Event-B.
 The only disadvantage of allowing reals is that the arithmetic operators
 are overloaded, which may require stronger typing.
 E.g., without ```x:INT``` you get an error that the type of x and y cannot be inferred, when reals are allowed:

 %% Cell type:code id:528e647d tags:

 ``` prob
 x:INT & x < y
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{x} = -1$
    * $\mathit{y} = 0$
    TRUE
    
    Solution:
    	x = −1
    	y = 0

 %% Cell type:markdown id:02b86510 tags:

 ### Constraint solving

 Constraint solving and enumeration is very limited in ProB.
 This will change in future.
 Currently ProB will enumerate a few random values for unspecified reals,
 and then stop with an enumeration warning.

 %% Cell type:code id:9356ea2c tags:

 ``` prob
 x:REAL
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{x} = 0.0$
    TRUE
    
    Solution:
    	x = 0.0

 %% Cell type:code id:b6d8671d tags:

 ``` prob
 x + 1.0 = 2.0
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{x} = 1.0$
    TRUE
    
    Solution:
    	x = 1.0

 %% Cell type:markdown id:13388af0 tags:

 ### Other Operators

 The standard library ```LibraryReals.def``` provides many functions
 over reals as external functions.
 These functions typically start with a capital R.
 The functions are available in the REPL (aka console) but
 one needs to import ```LibraryReals.def``` to use them in a B machine.

 %% Cell type:code id:df6d2cd0 tags:

 ``` prob
 RSQRT(2.0)
 ```

 %% Output

    $1.4142135623730951$
    1.4142135623730951

 %% Cell type:code id:d2daab50 tags:

 ``` prob
 RSIN(RPI)
 ```

 %% Output

    $1.2246467991473532E-16$
    1.2246467991473532E-16

 %% Cell type:code id:481e4f68 tags:

 ``` prob
 r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=0.5
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{r} = 1.0$
    * $\mathit{x} = 0.5$
    TRUE
    
    Solution:
    	r = 1.0
    	x = 0.5

 %% Cell type:code id:bfd74a24 tags:

 ``` prob
 r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=10.5
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{r} = 1.0$
    * $\mathit{x} = 10.5$
    TRUE
    
    Solution:
    	r = 1.0
    	x = 10.5

 %% Cell type:code id:34ca2773 tags:

 ``` prob
 REULER
 ```

 %% Output

    $2.718281828459045$
    2.718281828459045

 %% Cell type:code id:4b24407f tags:

 ``` prob
 RSIGN(-2.2)
 ```

 %% Output

    $-1.0$
    −1.0

 %% Cell type:code id:ec855071 tags:

 ``` prob
 RABS(-2.2)
 ```

 %% Output

    $2.2$
    2.2

 %% Cell type:code id:c0bf9060 tags:

 ``` prob
 RLOG(2.0,1024.0)
 ```

 %% Output

    $10.0$
    10.0

 %% Cell type:code id:152d2052 tags:

 ``` prob
 RLOGe(REULER)
 ```

 %% Output

    $1.0$
    1.0

 %% Cell type:code id:0a81f12f tags:

 ``` prob
 RMAX(1.4,RSQRT(2.0))
 ```

 %% Output

    $1.4142135623730951$
    1.4142135623730951

 %% Cell type:code id:4669fcd2 tags:

 ``` prob
 RONE+RZERO
 ```

 %% Output

    $1.0$
    1.0

 %% Cell type:markdown id:8df6222b tags:

 There are also external functions which are equivalent to the arithmetic operators: RLEQ, RGEQ, RLT, RGT, ROUND, RINTEGER, RADD, RSUB, RMUL, RDIV.
 This can be useful in some cases (e.g., when ALLOW_REALS is false or when mapping Event-B operators to classical B, see below).

 %% Cell type:markdown id:cc7e1768 tags:

+## Event-B Theories
+Event-B does not have support for reals or floats as basic type but one can use the theory plugin.
+
+[https://prob.hhu.de/w/index.php?title=Event-B_Theories]
+
+To be able to view reals in ProB within Rodin you need to install a recent nightly build: [https://www3.hhu.de/stups/rodin/prob1/nightly]
+
+You need to use one of the standard theories.
+
+To write your own theory you should add an axiomatic type called REAL, FLOAT or the unicode R for reals.
+Then you have to define axiomatic operators and link them to ProB's real operators.
+You can do this either
+* using a theory mapping file (.ptm extension) which needs to be put into the Rodin project, see [https://prob.hhu.de/w/index.php?title=Event-B_Theories]
+* or use the same name as the external functions above (e.g., RSQRT); in this way ProB will do the mapping automatically.
+
+