{ "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": "6caf3504", "metadata": {}, "source": [ "### Conversion Operators\n", "The following conversion operators are available in classical B:\n", "* floor\n", "* ceiling\n", "* real" ] }, { "cell_type": "code", "execution_count": 22, "id": "8925f6fe", "metadata": { "vscode": { "languageId": "plaintext" } }, "outputs": [ { "data": { "text/markdown": [ "$2.0$" ], "text/plain": [ "2.0" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "real(2)" ] }, { "cell_type": "code", "execution_count": 23, "id": "bbd73954", "metadata": { "vscode": { "languageId": "plaintext" } }, "outputs": [ { "data": { "text/markdown": [ "$2$" ], "text/plain": [ "2" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "floor(2.2)" ] }, { "cell_type": "code", "execution_count": 24, "id": "838ea786", "metadata": { "vscode": { "languageId": "plaintext" } }, "outputs": [ { "data": { "text/markdown": [ "$3$" ], "text/plain": [ "3" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "ceiling(2.2)" ] }, { "cell_type": "code", "execution_count": 25, "id": "ee31f934", "metadata": { "vscode": { "languageId": "plaintext" } }, "outputs": [ { "data": { "text/markdown": [ "$-2$" ], "text/plain": [ "−2" ] }, "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ "ceiling(-2.2)" ] }, { "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": 13, "id": "34ca2773", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$2.718281828459045$" ], "text/plain": [ "2.718281828459045" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "REULER" ] }, { "cell_type": "code", "execution_count": 14, "id": "4b24407f", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$-1.0$" ], "text/plain": [ "−1.0" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "RSIGN(-2.2)" ] }, { "cell_type": "code", "execution_count": 21, "id": "ec855071", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$2.2$" ], "text/plain": [ "2.2" ] }, "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "RABS(-2.2)" ] }, { "cell_type": "code", "execution_count": 17, "id": "c0bf9060", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$10.0$" ], "text/plain": [ "10.0" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "RLOG(2.0,1024.0)" ] }, { "cell_type": "code", "execution_count": 18, "id": "152d2052", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$1.0$" ], "text/plain": [ "1.0" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "RLOGe(REULER)" ] }, { "cell_type": "code", "execution_count": 19, "id": "0a81f12f", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$1.4142135623730951$" ], "text/plain": [ "1.4142135623730951" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "RMAX(1.4,RSQRT(2.0))" ] }, { "cell_type": "code", "execution_count": 20, "id": "4669fcd2", "metadata": { "vscode": { "languageId": "classicalb" } }, "outputs": [ { "data": { "text/markdown": [ "$1.0$" ], "text/plain": [ "1.0" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "RONE+RZERO" ] }, { "cell_type": "markdown", "id": "8df6222b", "metadata": {}, "source": [ "There are also external functions which are equivalent to the arithmetic operators: RLEQ, RGEQ, RLT, RGT, ROUND, RINTEGER, RADD, RSUB, RMUL, RDIV.\n", "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", "metadata": {}, "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": { "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 }