Quelle  IEEE_854_fp_int.pvs

IEEE_854_fp_int
  [b,p:above(1),
   alpha,E_max:integer, 
   E_min:{i:integer|E_max>i}]: THEORY


  BEGIN

  importing IEEE_854_values[b,p,E_max,E_min],
            real_to_fp[b,p,alpha,E_max,E_min],
            round

  fin, fin1: var (finite?)

  mode: var rounding_mode

  fp_to_int(fin,mode):integer = round(value(fin),mode)

  fp_to_int_fp(fin,mode): fp_num = 
       real_to_fp(round(value(fin),mode))


%  large_value: lemma  
%      abs(value(fin)) >= b^p => integer?(value(fin))
%
%  fp_to_int_fp_finite: lemma
%       E_max>p => finite?(real_to_fp(round(value(fin),mode)))

  END IEEE_854_fp_int