Commit fe2dcfe7 authored by MARCHE Claude's avatar MARCHE Claude

missing file

parent bf1abbb6
module Single
use import real.RealInfix
use export ieee_float.Float32
predicate add_pre_ieee (x:t) (y:t) =
t'isFinite (x .+ y)
predicate add_post_ieee (x:t) (y:t) (r:t) =
r = x .+ y
predicate add_pre_real (x:t) (y:t) =
no_overflow RNE (t'real x +. t'real y)
predicate add_post_real (x:t) (y:t) (r:t) =
t'real r = round RNE (t'real x +. t'real y)
val add (x y: t) : t
requires { "expl:floating-point overflow"
add_pre_ieee x y \/ add_pre_real x y }
ensures { add_post_ieee x y result /\ add_post_real x y result }
predicate sub_pre_ieee (x:t) (y:t) =
t'isFinite (x .- y)
predicate sub_post_ieee (x:t) (y:t) (r:t) =
r = x .- y
predicate sub_pre_real (x:t) (y:t) =
no_overflow RNE (t'real x -. t'real y)
predicate sub_post_real (x:t) (y:t) (r:t) =
t'real r = round RNE (t'real x -. t'real y)
val sub (x y: t) : t
requires { "expl:floating-point overflow"
sub_pre_ieee x y \/ sub_pre_real x y }
ensures { sub_post_ieee x y result /\ sub_post_real x y result }
predicate mul_pre_ieee (x:t) (y:t) =
t'isFinite (x .* y)
predicate mul_post_ieee (x:t) (y:t) (r:t) =
r = x .* y
predicate mul_pre_real (x:t) (y:t) =
no_overflow RNE (t'real x *. t'real y)
predicate mul_post_real (x:t) (y:t) (r:t) =
t'real r = round RNE (t'real x *. t'real y)
val mul (x y: t) : t
requires { "expl:floating-point overflow"
mul_pre_ieee x y \/ mul_pre_real x y }
ensures { mul_post_ieee x y result /\ mul_post_real x y result }
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment