add float/reals manual

notebooks/manual/FloatsReals.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "85001897",
+   "metadata": {},
+   "source": [
+    "# Reals and Floats in ProB\n",
+    "\n",
+    "### Michael Leuschel\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "42473a5e",
+   "metadata": {},
+   "source": [
+    "## Classical B\n",
+    "\n",
+    "In Atelier-B the following two types were added to the B language:\n",
+    "* REAL\n",
+    "* FLOAT\n",
+    "\n",
+    "ProB treats these keywords as synonyms for a new base type.\n",
+    "The current representation in ProB are floating point numbers; but this\n",
+    "will probably change in the future, at least for the REAL type.\n",
+    "\n",
+    "One can now also use literals in decimal point notation for REAL and FLOAT."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "id": "cf76baf3",
+   "metadata": {
+    "vscode": {
+     "languageId": "plaintext"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1.0$"
+      ],
+      "text/plain": [
+       "1.0"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "1.0"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "id": "941433ba",
+   "metadata": {
+    "vscode": {
+     "languageId": "plaintext"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "1.0 : REAL & 1.0 : FLOAT"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "f7398e0e",
+   "metadata": {},
+   "source": [
+    "### Arithmetic Operators\n",
+    "\n",
+    "The documentation of Atelier-B is not entirely consistent according to which\n",
+    "operators to use.\n",
+    "In ProB you can use the standard arithmetic operators also for\n",
+    "floats:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "65a66ec9",
+   "metadata": {
+    "vscode": {
+     "languageId": "plaintext"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$2.0$"
+      ],
+      "text/plain": [
+       "2.0"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "1.0 + 1.0"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "35ce95d5",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "2.0 * 2.0 < 2.1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "531aa72d",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "2.0 * 2.0 < 2.0 + 2.0"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "9066aa50",
+   "metadata": {},
+   "source": [
+    "You can control whether to allow arithmetic operators for reals\n",
+    "in ProB via the preference ```ALLOW_REALS```.\n",
+    "By default reals are allowed for classical B and disallowed for Event-B.\n",
+    "The only disadvantage of allowing reals is that the arithmetic operators\n",
+    "are overloaded, which may require stronger typing.\n",
+    "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",
+   "execution_count": 4,
+   "id": "528e647d",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{x} = -1$\n",
+       "* $\\mathit{y} = 0$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tx = −1\n",
+       "\ty = 0"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x:INT & x < y"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "02b86510",
+   "metadata": {},
+   "source": [
+    "### Constraint solving\n",
+    "\n",
+    "Constraint solving and enumeration is very limited in ProB.\n",
+    "This will change in future.\n",
+    "Currently ProB will enumerate a few random values for unspecified reals,\n",
+    "and then stop with an enumeration warning."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "id": "9356ea2c",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{x} = 0.0$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tx = 0.0"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x:REAL"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "id": "b6d8671d",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{x} = 1.0$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tx = 1.0"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x + 1.0 = 2.0"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "13388af0",
+   "metadata": {},
+   "source": [
+    "### Other Operators\n",
+    "\n",
+    "The standard library ```LibraryReals.def``` provides many functions\n",
+    "over reals as external functions.\n",
+    "These functions typically start with a capital R.\n",
+    "The functions are available in the REPL (aka console) but\n",
+    "one needs to import ```LibraryReals.def``` to use them in a B machine.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "id": "df6d2cd0",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1.4142135623730951$"
+      ],
+      "text/plain": [
+       "1.4142135623730951"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "RSQRT(2.0)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "id": "d2daab50",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1.2246467991473532E-16$"
+      ],
+      "text/plain": [
+       "1.2246467991473532E-16"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "RSIN(RPI)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "id": "481e4f68",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{r} = 1.0$\n",
+       "* $\\mathit{x} = 0.5$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr = 1.0\n",
+       "\tx = 0.5"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=0.5"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "id": "bfd74a24",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{r} = 1.0$\n",
+       "* $\\mathit{x} = 10.5$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr = 1.0\n",
+       "\tx = 10.5"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=10.5"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "34ca2773",
+   "metadata": {
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "codemirror_mode": "prob2_jupyter_repl",
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob2-jupyter-repl",
+   "name": "prob"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}