Quelle over_under.pvs Sprache: PVS

over_under
  [b,p:above(1),
   alpha,E_max:integer,
   E_min:{i:integer|E_max>i}]: THEORY

  BEGIN

  IMPORTING IEEE_854_values[b,p,E_max,E_min],
            fp_round_aux[b,p],
            enumerated_type_defs,
            round

  over_under?(r:real): bool = (r/=0 & (abs(r)>max_pos or abs(r)<b^E_min))

% A real number that real_to_fp maps to infinity
  infinity: real = b^(E_max+1)

  trap_over((r1:nzreal), (r2: real), (mode: rounding_mode)): real =
    IF trap_enabled?(overflow) THEN round_scaled(r1 * b ^ (-alpha), mode)
    ELSE r2
    ENDIF

  overflow((r: nzreal | abs(r) > max_pos), (mode: rounding_mode)):
      [real, exception] =
    CASES mode OF
      to_nearest:
          IF abs(r)
                >= b ^ (E_max + 1)
                     - (1 / 2) * b ^ (E_max + 1 - p)
            THEN (trap_over(r, (sgn(r) * infinity), mode),overflow)
          ELSE (sgn(r) * max_pos, inexact)
          ENDIF,
      to_zero:
          IF abs(r) >= b ^ (E_max + 1)
            THEN (trap_over(r, (sgn(r) * max_pos), mode),overflow)
          ELSE (sgn(r) * max_pos, inexact)
          ENDIF,
      to_pos:
          IF r > max_pos THEN (trap_over(r, infinity, mode),overflow)
          ELSIF r <= -b ^ (E_max + 1)
            THEN (trap_over(r, max_neg, mode),overflow)
          ELSE (max_neg, inexact)
          ENDIF,
      to_neg:
          IF r < max_neg THEN (trap_over(r, -infinity, mode),overflow)
          ELSIF r >= b ^ (E_max + 1)
            THEN (trap_over(r, max_pos, mode),overflow)
          ELSE (max_pos, inexact)
          ENDIF
      ENDCASES

  tiny_flag: bool % = true for tininess detected after rounding
  inaccurate_flag: bool % = true for inaccurate detected using first option

  exact_underflow((r:nzreal|abs(r)<b^E_min),mode:rounding_mode):bool =
       (r*b^alpha=round_scaled(r*b^alpha,mode))

  %implicitly already have tininess detected before rounding
  tiny?((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): bool =
    IF tiny_flag THEN abs(round_scaled(r, mode)) < b ^ E_min ELSE TRUE ENDIF

  round_under((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): real
    = b^(E_min - (p - 1))*round(b^(-(E_min - (p - 1)))*r,mode)

  mode: var rounding_mode

  round_under_correct: LEMMA
        round_under(min_pos,mode) = min_pos

  fin: var (finite?)

  round_under_value: lemma subnormal?(fin) =>
                 round_under(value(fin),mode) = value(fin)

  r:var nzreal

  round_under_error: LEMMA
        abs(r) < b ^ E_min
          => abs(r - round_under(r, mode)) < b ^ (E_min - (p - 1))

  round_under_near: LEMMA
        abs(r) < b ^ E_min
          => abs(r - round_under(r, to_nearest)) <= b ^ (E_min - (p - 1)) / 2

  round_under_pos: lemma abs(r)<b^E_min => round_under(r,to_pos)>=r

  round_under_neg: lemma abs(r)<b^E_min => round_under(r,to_neg)<=r

  round_under_zero: lemma abs(r)<b^E_min => abs(round_under(r,to_zero))<=abs(r)

  inaccurate?((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): bool =
    IF inaccurate_flag THEN (round_scaled(r,mode)/=round_under(r,mode))
    ELSE (r/=round_under(r,mode))
    ENDIF

  underflow((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)):
      [real, exception] =
    IF tiny?(r, mode)
      THEN IF trap_enabled?(underflow(FALSE))
        THEN (round_scaled(r * b ^ alpha, mode),
              underflow(exact_underflow(r, mode)))
      ELSIF inaccurate?(r, mode) THEN (round_under(r, mode), underflow(TRUE))
      ELSE (round_under(r, mode),
            IF r = round_under(r, mode) THEN no_exceptions
            ELSE inexact
            ENDIF)
      ENDIF
    ELSE (round_under(r, mode), inexact)
    ENDIF

  END over_under

quality100%

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