1 files changed, 79 insertions, 0 deletions
diff --git a/fp_documentation.txt b/fp_documentation.txt
new file mode 100644
index 00000000..09e60b9a
--- /dev/null
+++ b/fp_documentation.txt
@@ -0,0 +1,79 @@
+Floating Point Documentation for Boogie
+Written by Dietrich Geisler
+Contact: dgeisler50@gmail.com
+
+This document aims to describe the syntax for declaring and using floating points in Boogie
+
+--------------------------------------------------------------------------------
+Declaring Variables:
+
+The syntax for declaring a floating point variable is as follows:
+var name: float(exp man);
+Where exp is the size of the float exponent and man is the size of the float mantissa
+
+It is also acceptable to use the following syntax:
+var name: float();
+This syntax assumes the float exponent to be size 8 and the mantissa to be size 24
+
+example:
+var x: float(11 53)
+Declares a variable called x with a exponent sized 11 and mantissa sized 53
+
+--------------------------------------------------------------------------------
+Declaring Constants:
+
+All of the following syntax are viable for declaring a floating point constant:
+float(dec)
+float(exp_val man_val)
+float(dec exp man)
+float(exp_val man_val exp man)
+
+Where dec is the decimal value of the constant,
+exp_val/man_value are the integer values of their respective fields,
+And exp/man are the sizes of their respective fields.
+Note that when exp and man are not specified, they are given sizes 8 and 24 respectively
+
+--------------------------------------------------------------------------------
+Defined Operations:
+
+Given two floating point values x and y with the same size of exponent and mantissa
+The following operations operate as defined in Operators section of this document:
+http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml
+(Note that rounding mode is always assumed to be Round to Nearest Even (RNE))
+(Also note that operations not listed here are undefined)
+
+operatation		boogie syntax
+neg(x)			-x
+add(x, y)		x + y
+sub(x, y)		x - y
+mul(x, y)		x * y
+div(x, y)		x / y
+leq(x, y)		x <= y
+lt(x, y)		x < y
+geq(x, y)		x >= y
+gt(x, y)		x > y
+eq(x, y)		x == y
+
+--------------------------------------------------------------------------------
+Other:
+
+The following special values can be declared with the following syntax:
+Value		Declaration
+NaN			fp(nan exp man)
++oo			fp(oo exp man) OR fp(INF exp man)
+-oo			fp(-oo exp man) OR fp(INF exp man)
+-zero		fp(-zero exp man)
+Where exp and man are the sizes of the exponent and mantissa respectively
+
+--------------------------------------------------------------------------------
+Known Issues:
+
+There is currently no way to convert from a floating point to any other data type
+
+There is currently no way to convert the value of a variable to a floating point type
+For example, the following statements fails:
+var x : real;
+fp(x);
+
+Statements of the following form cause a parser error (parenthesis followed by fp constant)
+... (fp(1) + fp(1));
+\ No newline at end of file