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.''
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Assumption about balanced exponents as given in standard % (comment out if you do not desire this constraint)
