Commit c6787174 authored by Antonin Dudermel's avatar Antonin Dudermel
Browse files

lsb version 2.0

parent a297acf9
process = _ <: *(15), _ <: <(12), *(4), >=(12), *(.25) + .75: *, * :> _ ;
process = _ <: *(15), _ <:
<(12), *(4), >=(12), *(.25) + .75:
*, * :> _ ;
@rnd = float<ieee_32, ne>;
x = rnd(xx);
t rnd= (1 - x);
y rnd= x * t;
z = x * (1 - x);
@rnd = float<ieee_32, ne>; # definition of a rounding mode
x = rnd(xx); # the input value itself is a FP number
t rnd= (1 - x); # one intermediate value of the code
y rnd= x * t; # another line describing what is computed
z = x * (1 - x); # this is the mathematical ideal value
# without rounding
{ x in [0, 1] -> y in ? /\ z - y in ? }
{ x in [0, 1] -> y in ? /\ z - y in ? } # the theorem to prove
z -> 0.25 - (x - 0.5) * (x - 0.5);
This diff is collapsed.
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