Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: fp_round_aux.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.