Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: IEEE_854_values.pvs Sprache: PVS

Original von: PVS^©

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This file defines the set of values that must be represented in each
% supported precision of an instance of IEEE-854
%
% Author:
%  Paul S. Miner                | email: [email protected]
%  1 South Wright St. / MS 130  |   fax: (757) 864-4234
%  NASA Langley Research Center | phone: (757) 864-6201
%  Hampton, Virginia 23681      |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  BEGIN

  IMPORTING sum_hack, %for use until we have good summation library
            sum_lemmas[b], % these are more specialized
%            ints@mod_, %% note _ to avoid prelude version
            enumerated_type_defs

  Exponent: type = {i:int| E_min <= i & i <= E_max}

  digits: type = [below(p)->below(b)]

  fp_num: datatype
   begin
    finite(sign:sign_rep,Exp:Exponent,d:digits):finite?
    infinite(i_sign:sign_rep): infinite?
    NaN(status:NaN_type, data:NaN_data): NaN?
   end fp_num

% A mapping from finite floating point numbers to real numbers
%  This corresponds to the interpretation given in the standard
%  section 3.1
  fin : var (finite?)

  value_digit(d:digits)(n:nat):nonneg_real =
     if n<p then d(n)*b^(-n) else 0 endif

  value(fin): real =
    (-1) ^ sign(fin) * b ^ Exp(fin) * Sum(p, value_digit(d(fin)))

% Predicate testing whether an fp_num is 0
  zero?(fp:fp_num):bool = if finite?(fp) then value(fp)=0 else false endif

  shift_left((d: digits)): digits =
    LAMBDA (i: below(p)): IF (i + 1 = p) THEN 0 ELSE d(i + 1) ENDIF

% Function normalize takes a finite and returns the finite of
% equivalent value with the smallest possible exponent.
  normalize(fin:(finite?)): recursive (finite?) =
     IF Exp(fin) = E_min or d(fin)(0) /= 0 then
        fin
     ELSE
        normalize(finite(sign(fin),Exp(fin)-1,shift_left(d(fin))))
     ENDIF
  measure lambda (fin:(finite?)): Exp(fin) - E_min

  normalize_idempotent: FACT
        FORALL (fin: (finite?)): normalize(normalize(fin)) = normalize(fin)

% Predicate testing whether an fp_num is subnormal:
% Section 2 of the standard defines a subnormal (denormal in IEEE-754)
% number as a nonzero finite number whose exponent is the precision's
% minimum and whose leading significant digit is zero.
  subnormal?(fp: fp_num): bool =
    IF finite?(fp)  THEN
        not zero?(fp)
        & Exp(normalize(fp)) = E_min
        & d(normalize(fp))(0) = 0
    ELSE FALSE
    ENDIF

% Predicate testing whether an fp_num is normal:
% Section 2 of the standard defines a normal number as
% a nonzero finite number that is not subnormal
  normal?((fp: fp_num)): bool =
    IF finite?(fp) THEN d(normalize(fp))(0) > 0 ELSE FALSE ENDIF

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some definitions and theorems to help illustrate the correctness
%  of the definition of value.

% Maximum and Minimum representable values
  max_significand:digits =
    (lambda (i:below(p)): b-1)
  min_significand: digits =
    (LAMBDA (i: below(p)): IF i < p - 1 THEN 0 ELSE 1 ENDIF)
  d_zero: digits = LAMBDA (i: below(p)): 0

  m,n: var nat

  Sum_value0: lemma Sum(n,value_digit(d_zero)) = 0

  s: var sign_rep
  E: var Exponent

  zero_finite_d_zero: lemma zero?(finite(s,E,d_zero))

  max_fp_pos : fp_num = finite(pos,E_max,max_significand)
  min_fp_pos : fp_num = finite(pos,E_min,min_significand)
  pos_zero   : {fin|zero?(fin)}= finite(pos,E_min,d_zero)

  max_fp_neg : fp_num = finite(neg,E_max,max_significand)
  min_fp_neg : fp_num = finite(neg,E_min,min_significand)
  neg_zero   : {fin|zero?(fin)} = finite(neg,E_min,d_zero)

  max_pos: posreal = value(max_fp_pos)
  min_pos: posreal = value(min_fp_pos)

  max_neg: negreal = value(max_fp_neg)
  min_neg: negreal = value(min_fp_neg)

  max_fp_correct: THEOREM
     max_pos = b ^ (E_max +1) - b ^ (E_max + 1 - p)

  min_fp_correct: THEOREM
     value(min_fp_pos) = b ^ (E_min + 1 - p)

% Value of zero

  value0: lemma value(fin)=0 iff d(fin)=d_zero

  value_of_zero: THEOREM
     value(pos_zero) = 0

% Normalization preserves the value

  normal_value: lemma
     value(fin) = value(normalize(fin))

% sign determines algebraic sign of value
  value_positive: lemma

    (sign(fin)=pos & not zero?(fin)) <=> value(fin)>0

  value_negative: lemma
    (sign(fin)=neg & not zero?(fin)) <=> value(fin)<0

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  finite_cover: lemma zero?(fin) or normal?(fin) or subnormal?(fin)

  finite_disjoint1: lemma not (zero?(fin) & normal?(fin))

  finite_disjoint2: lemma not (zero?(fin) & subnormal?(fin))

  finite_disjoint3: lemma not (normal?(fin) & subnormal?(fin))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
  fp,fp1,fp2: var fp_num

% reverse the sign of a floating point number
  toggle_sign(fp): fp_num
    =
    cases fp of
      finite(s,e,d): finite(1-s,e,d),
      infinite(s): infinite(1-s),
      NaN(sig,data): fp
    endcases

  toggle_finite: lemma finite?(toggle_sign(fp)) iff finite?(fp)
  toggle_infinite: lemma infinite?(toggle_sign(fp)) iff infinite?(fp)
  toggle_NaN: lemma NaN?(toggle_sign(fp)) iff NaN?(fp)

  value_toggle: lemma value(toggle_sign(fin)) = -value(fin)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  toggle_d_normalize: lemma
     d(normalize(toggle_sign(fin))) = d(normalize(fin))

  toggle_Exp_normalize: lemma
     Exp(normalize(toggle_sign(fin))) = Exp(normalize(fin))

  toggle_zero?: lemma zero?(toggle_sign(fin)) iff zero?(fin)

  toggle_normal?: lemma normal?(toggle_sign(fin)) iff normal?(fin)

  toggle_subnormal?: lemma subnormal?(toggle_sign(fin)) iff subnormal?(fin)

% Sum lemmas

  d: var digits

  j : var nat

  value_digit_le: lemma value_digit(d)(j) <= (b-1) * b^(-j)

  Sum_d_lt_b: lemma Sum(j+1,value_digit(d)) <= b - b^(-j)

  Sum_d_lt1: lemma d(0)=0 => Sum(j+1,value_digit(d)) <= 1-b^(-j)

  Sum_d_ge1: lemma d(0)>0 => Sum(j+1,value_digit(d)) >= 1

  value_sig_lt_b: lemma Sum(p,value_digit(d)) < b

  value_sig_lt1: lemma d(0)=0 => Sum(p,value_digit(d)) < 1

  value_sig_ge1: lemma d(0)>0 => Sum(p,value_digit(d)) >= 1

  abs_value_fin: lemma
      abs(value(fin)) = b^(Exp(fin)) * Sum(p,value_digit(d(fin)))

  min_significand_min: lemma d/=d_zero =>
            Sum(p,value_digit(min_significand))<= Sum(p,value_digit(d))

  sign_normal: lemma sign(fin) = sign(normalize(fin))

  value_normal: lemma normal?(fin) =>
            b^E_min <= abs(value(fin)) & abs(value(fin)) <= max_pos

  value_subnormal: lemma subnormal?(fin) =>
            min_pos <= abs(value(fin)) & abs(value(fin)) < b^E_min

  value_nonzero: lemma not zero?(fin) =>
            min_pos <= abs(value(fin)) & abs(value(fin)) <= max_pos

%mod(floor(Sum(p, value_digit(d(normalize(fin!1)))) * b ^ x!1), b)
%        = d(normalize(fin!1))(x!1)

    scale_value(d,m)(n): nonneg_real = value_digit(d)(n) * b^m

    scaled_Sum_int: lemma forall d,n:
       forall (m:upto(n+1)): integer?(Sum(m,scale_value(d,n)))

    scale_value_p(d)(n): nat = scale_value(d,p-1)(n)

    i: var below(p)

    scaled_Sum_i: lemma
        Sum(n,value_digit(d))*b^(i) = Sum(n,scale_value(d,i))

    scaled_Sum: lemma
        Sum(n,value_digit(d))*b^(p-1) = Sum(n,scale_value_p(d))

    floor_Sum: lemma
        floor(Sum(p,value_digit(d)) * b^i) =
             Sum(i+1,scale_value(d,i))

    mod_Sum: lemma mod(Sum(i+1,scale_value(d,i)),b)=d(i)

%%%%%%%%%
%
%  The next two declarations are here for importing purposes.

% A dummy fp_num to be used as a place holder.  Any definition that
% returns holder is not yet finished.
  holder:fp_num

% An undefined NaN for functions to return when the invalid exception
% should be raised.  This serves as a placeholder until this specification
% accounts for exceptions.
%
  invalid: (NaN?) = NaN(quiet,invalid_data)

  END IEEE_854_values

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.