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

Copyright(c) Levent Erkok
Safe HaskellNone




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.


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


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

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

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
>>> (-3.7777752e22 + ((-1.180801e18) + 9.4447324e21)) :: Float

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)


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

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)