sbv-3.4: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Examples.Misc.Floating

Contents

Description

Several examples involving IEEE-754 floating point numbers, i.e., single precision Float (SFloat) and double precision Double (SDouble) types.

Note that arithmetic with floating point is full of surprises; due to precision issues associativity of arithmetic operations typically do not hold. Also, the presence of NaN is always something to look out for.

Synopsis

FP addition is not associative

assocPlus :: SFloat -> SFloat -> SFloat -> SBool Source

Prove that floating point addition is not associative. We have:

>>> prove assocPlus
Falsifiable. Counter-example:
  s0 = -7.888609e-31 :: SFloat
  s1 = 3.944307e-31 :: SFloat
  s2 = NaN :: SFloat

Indeed:

>>> let i = 0/0 :: Float
>>> ((-7.888609e-31 + 3.944307e-31) + i) :: Float
NaN
>>> (-7.888609e-31 + (3.944307e-31 + i)) :: Float
NaN

But keep in mind that NaN does not equal itself in the floating point world! We have:

>>> let nan = 0/0 :: Float in nan == nan
False

assocPlusRegular :: IO ThmResult Source

Prove that addition is not associative, even if we ignore NaN/Infinity values. To do this, we use the predicate isFPPoint, which is true of a floating point number (SFloat or SDouble) if it is neither NaN nor Infinity. (That is, it's a representable point in the real-number line.)

We have:

>>> assocPlusRegular
Falsifiable. Counter-example:
  x = -3.7777752e22 :: SFloat
  y = -1.180801e18 :: SFloat
  z = 9.4447324e21 :: SFloat

Indeed, we have:

>>> ((-3.7777752e22 + (-1.180801e18)) + 9.4447324e21) :: Float
-2.83342e22
>>> (-3.7777752e22 + ((-1.180801e18) + 9.4447324e21)) :: Float
-2.8334201e22

Note the loss of precision in the first expression.

FP addition by non-zero can result in no change

nonZeroAddition :: IO ThmResult Source

Demonstrate that a+b = a does not necessarily mean b is 0 in the floating point world, even when we disallow the obvious solution when a and b are Infinity. We have:

>>> nonZeroAddition
Falsifiable. Counter-example:
  a = 2.1474839e10 :: SFloat
  b = -7.275957e-11 :: SFloat

Indeed, we have:

>>> 2.1474839e10 + (-7.275957e-11) == (2.1474839e10 :: Float)
True

But:

>>> -7.275957e-11 == (0 :: Float)
False

FP multiplicative inverses may not exist

multInverse :: IO ThmResult Source

The last example illustrates that a * (1/a) does not necessarily equal 1. Again, we protect against division by 0 and NaN/Infinity.

We have:

>>> multInverse
Falsifiable. Counter-example:
  a = 1.2354518252390238e308 :: SDouble

Indeed, we have:

>>> let a =  1.2354518252390238e308 :: Double
>>> a * (1/a)
0.9999999999999998