Quelle fp_round_aux.pvs Sprache: PVS

fp_round_aux[b,p:above(1)]: THEORY

  BEGIN

  importing round,
%%%%%%%%%%%%%%%%% ajout S. Boldo
            %% ints@mod_,
%%%%%%%%%%%%%%%%% fin ajout
            enumerated_type_defs

  r: var real
  x: var posreal

  sign_of(r:real): sign_rep = IF r < 0 THEN neg ELSE pos ENDIF

  Exp_of(x:posreal): {i:int| b^i<= x & x < b^(i+1)}

  Exp_of_correct: lemma
      1 <= x*b^(-Exp_of(x)) & x*b^(-Exp_of(x)) < b

  norm_fp_range: type = {x:posreal | 1 <= x & x < b}

  n1: var norm_fp_range

  z: var nzreal

  E(z):integer = Exp_of(abs(z))

  significand(z):norm_fp_range = abs(z)*b^(-Exp_of(abs(z)))

  real_components: lemma
    z = sgn(z)* b^E(z) * significand(z)

  abs_real_components: LEMMA
    abs(z) = b^E(z)*significand(z)

  i,j: var integer

  Exp_of_unique: LEMMA
    b^i <= x & x < b^(i+1) & b^j<=x & x<b^(j+1) => i=j

  posreal_exponent: lemma
    x = b^i *n1 => E(x) = i

  real_exponent: lemma
    z = sgn(z)*b^i * n1 => E(z) = i

  scale(x:posreal):{i:int|b^(i+p-1)<=x & x < b^(i+p)} = Exp_of(x)-(p-1)

  scale_correct: lemma b^(p-1)<=x/b^scale(x) & x/b^scale(x)< b^p

  round_scaled(r:nzreal,mode:rounding_mode): real =
    b^(scale(abs(r)))*round( b^(-scale(abs(r)))*r,mode)

  E1: var integer
  px: var posreal
  nnx: var nonneg_real

  truncate(E1,nnx): [below(p)->below(b)] =
      (lambda (i:below(p)): mod(floor(b^(i-E1)*nnx),b))

  truncate_shift: LEMMA
    truncate(i,b^j*px) = truncate(i-j,px)

  Exp_of_shift: LEMMA
    Exp_of(b^j*px) = j + Exp_of(px)

  scale_shift: LEMMA
    scale(b^j*px) = j + scale(px)

  END fp_round_aux

quality93%

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