Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- import Data.SBV
- test1 :: (SFloat -> SFloat -> SFloat) -> Symbolic SBool
- test1 fun =
- do [x, y] <- sFloats ["x", "y"]
- constrain $ bnot (isInfiniteFP x) &&& bnot (isInfiniteFP y)
- constrain $ 0 .<= x &&& x .<= y
- let z = fun x y
- return $ x .<= z &&& z .<= y
- test2 :: (SFloat -> SFloat -> SFloat) -> Symbolic SBool
- test2 fun =
- do [x, y] <- sFloats ["x", "y"]
- constrain $ bnot (isInfiniteFP x) &&& bnot (isInfiniteFP y)
- constrain $ x .<= y
- let z = fun x y
- return $ x .<= z &&& z .<= y
- λ> prove $ test1 (x y -> (x + y) / 2)
- Falsifiable. Counter-example:
- x = 2.3089316e36 :: Float
- y = 3.379786e38 :: Float
- λ> prove $ test1 (x y -> x/2 + y/2)
- Falsifiable. Counter-example:
- x = 2.3509886e-38 :: Float
- y = 2.3509886e-38 :: Float
- λ> prove $ test1 (x y -> x + (y-x)/2)
- Q.E.D.
- λ> prove $ test2 (x y -> x + (y-x)/2)
- Falsifiable. Counter-example:
- x = -3.1300826e34 :: Float
- y = 3.402721e38 :: Float
- λ> prove $ test2 (x y -> x + (y/2 - x/2))
- Q.E.D.
- if max(abs(x),abs(y)) >= 1.:
- return x/2. + y/2.
- else:
- return (x+y)/2.
- float difference = max(x, y) - min(x, y);
- return min(x, y) + (difference / 2.0);
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement