1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
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)
|
