| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/float/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle IEEE_854.pvs Sprache: 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: p.s.miner@larc.nasa.gov % 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.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28