Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: max_below.pvs Sprache: PVS

Original von: PVS^©

IEEE_854 [b,p:above(1),alpha,E_max,E_min:integer]: THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  This theory defines the representation and basic operations for
%    arbitrary precision IEEE-854 floating point numbers.  It also
%    introduces the required assumption for arbitrary precision
%    IEEE-854 floating point numbers.
%
%  Example use:
%
%   To define IEEE-754 single-precision operations use the following
%     importing:
%
%     IMPORTING IEEE_854[2,24,192,127,-126]
%
%  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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Representation assumptions (from section 3.1 of IEEE-854)
  ASSUMING

    Base_values: ASSUMPTION b=2 or b=10

    Exponent_range: ASSUMPTION (E_max - E_min)/p > 5 %10 % may be 5

    Significand_size: ASSUMPTION b^(p-1)>=10^5

%  Uncomment the following, if you wish to include the suggestion
%   about exponent balance .

    E_balance: ASSUMPTION
        IF b < 4 THEN E_max + E_min = 1 ELSE E_max + E_min = 0 ENDIF

% Although not mentioned explicitly as a parameter.  We need the following
% value for adjusting the exponent of overflow and underflow results when the
% corresponing traps are enabled.

% Section 7.3 of IEEE-854 states: `` The exponent adjustment $\alpha$
% for a precision shall be chosen to be approximately
% $3\times(\Emax - \Emin)/4$ for that precision and should be
% divisible by twelve.''

    Exponent_Adjustment: ASSUMPTION
         abs(alpha - (3 * (E_max - E_min) / 4)) <= 6
          & integer?(alpha / 12)

  ENDASSUMING
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Assumption about balanced exponents as given in standard
%  (comment out if you do not desire this constraint)

  Exponent_balance: LEMMA b^(E_max+E_min) <4 & 4<=b^(E_max+E_min+1)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  A useful consequence of the assumptions

  E_max_gt_E_min: lemma E_max > E_min

  AUTO_REWRITE+ E_max_gt_E_min

% An illustrative example for HUG95 paper
  HUG_example: lemma 5*p < E_max-E_min  => E_min < E_max

% Simple examples showing how importing tccs may be automatically proven
  ex754_2:lemma (127 - (-126))/24 > 5

  ex754_3: lemma 2^23 >=10^5

% Some beneficial consequences of assumption E_balance
%  (These cannot be proven without E_balance)

  E_min_neg: lemma E_min<0

  E_max_pos: lemma E_max>0

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

  Importing IEEE_854_defs[b,p,alpha,E_max,E_min]



  END IEEE_854

¤ Dauer der Verarbeitung: 0.2 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.