From 29544b322eec0a0e630e2c7f8fe472793cf8f405 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 21:17:59 -0600 Subject: removed an unnecessary text file --- fp_documentation.txt | 88 ---------------------------------------------------- 1 file changed, 88 deletions(-) delete mode 100644 fp_documentation.txt diff --git a/fp_documentation.txt b/fp_documentation.txt deleted file mode 100644 index d3fafdcb..00000000 --- a/fp_documentation.txt +++ /dev/null @@ -1,88 +0,0 @@ -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 -Please note that - -**REMOVE THIS SYNTAX** -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: -**REMOVE THE FIRST OF THESE TWO SYNTAXES** -fp(dec) -fp(exp_val man_val) -fp(dec exp man) -fp(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: - -float16, float32, float64, and float128 still need to be added - -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)); - -Attempts by Boogie to infer the behavior of loops fail when floating points are involved - -Describing loop behavior manually is untested (using loop unroll appears to work) \ No newline at end of file -- cgit v1.2.3