Quelle round.pvs Sprache: 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: 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      |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%  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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.