|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
lyxvc.h
Sprache: C
Original von: PVS©
|
|
round: THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Defines type:
% rounding_mode: type = {to_nearest,to_zero,to_pos,to_neg}
%
% Defines functions:
%
% round: [[real,rounding_mode] -> integer]
%
% Rounds a real number to the nearest integer in accordance
% with the rounding mode (as specified in IEEE-854).
% The function round can be used in two parts of the IEEE-854
% floating point standard.
% 1.) Round floating point to integral value (section 5.5)
% or for converting a floating point to integer (5.4).
% 2.) By giving function `round' an appropriately scaled
% argument, this function can be used in the process
% of converting a real number to a floating point
% representation.
%
% round_to_even:[real -> integer]
%
% Auxilliary function used in definition of round. Selects the
% integer nearest in value to the real argument.
% If the real number is exactly halfway between two integers,
% this function selects the nearest even integer.
% Can also be used:
% -- As an auxilliary function in the definition of
% the remainder function (section 5.1). For y/=0,
% x REM y =def= x - y*n, where n = round_to_even(x/y).
%
%
% 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 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Requires library `floor'
BEGIN
importing enumerated_type_defs
% rounding_mode:type = {to_nearest,to_zero,to_pos,to_neg}
mode: var rounding_mode
r: VAR real
round_to_even(r): integer =
IF r - floor(r) < ceiling(r) - r THEN floor(r)
ELSIF ceiling(r) - r < r - floor(r) THEN ceiling(r)
ELSIF floor(r) = ceiling(r) THEN floor(r)
ELSE 2 * floor(ceiling(r) / 2)
ENDIF
round_to_even0: lemma round_to_even(0)=0
round_to_even1: LEMMA abs(r - round_to_even(r)) <= 1 / 2
round_to_even2: LEMMA
abs(r - round_to_even(r)) = 1 / 2 => integer?(round_to_even(r) / 2)
round(r,mode): integer =
CASES mode of
to_nearest: round_to_even(r),
to_zero: sgn(r) * floor(abs(r)),
to_pos: ceiling(r),
to_neg: floor(r)
ENDCASES
round1: LEMMA abs(r-round(r,mode))<1
i:var int
round_int: LEMMA round(i,mode)=i
END round
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
