Single.pvs 3.82 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
Single: THEORY
 BEGIN
  IMPORTING int@Int
  IMPORTING real@Real
  IMPORTING real@Abs
  IMPORTING real@FromInt
  IMPORTING Rounding
  IMPORTING SingleFormat
  % do not edit above this line
  
  % Why3 round
  round(x:Rounding.mode, x1:real): real
  
  % Why3 round_logic
  round_logic(x:Rounding.mode, x1:real): SingleFormat.single
  
  % Why3 value
  value(x:SingleFormat.single): real
  
  % Why3 exact
  exact(x:SingleFormat.single): real
  
  % Why3 model
  model(x:SingleFormat.single): real
  
  % Why3 round_error
  round_error(x:SingleFormat.single): real = abs((value(x) - exact(x)))
  
  % Why3 total_error
  total_error(x:SingleFormat.single): real = abs((value(x) - model(x)))
  
  % Why3 no_overflow
  no_overflow(m:Rounding.mode, x:real): bool = (abs(round(m,
    x)) <= SingleFormat.max_single)
  
  % Why3 bounded_real_no_overflow
  bounded_real_no_overflow: LEMMA FORALL (m:Rounding.mode, x:real):
    (abs(x) <= SingleFormat.max_single) => no_overflow(m, x)
  
  % Why3 round_monotonic
  round_monotonic: LEMMA FORALL (m:Rounding.mode, x:real, y:real):
    (x <= y) => (round(m, x) <= round(m, y))
  
  % Why3 round_idempotent
  round_idempotent: LEMMA FORALL (m1:Rounding.mode, m2:Rounding.mode,
    x:real): (round(m1, round(m2, x)) = round(m2, x))
  
  % Why3 round_value
  round_value: LEMMA FORALL (m:Rounding.mode, x:SingleFormat.single):
    (round(m, value(x)) = value(x))
  
  % Why3 bounded_value
  bounded_value: LEMMA FORALL (x:SingleFormat.single):
    (abs(value(x)) <= SingleFormat.max_single)
  
  % Why3 exact_rounding_for_integers
  exact_rounding_for_integers: LEMMA FORALL (m:Rounding.mode, i:int):
    (((-SingleFormat.max_int) <= i) AND (i <= SingleFormat.max_int)) =>
    (round(m, (i :: real)) = (i :: real))
  
  % Why3 round_down_le
  round_down_le: LEMMA FORALL (x:real): (round(Rounding.down, x) <= x)
  
  % Why3 round_up_ge
  round_up_ge: LEMMA FORALL (x:real): (round(Rounding.up, x) >= x)
  
  % Why3 round_down_neg
  round_down_neg: LEMMA FORALL (x:real): (round(Rounding.down,
    (-x)) = (-round(Rounding.up, x)))
  
  % Why3 round_up_neg
  round_up_neg: LEMMA FORALL (x:real): (round(Rounding.up,
    (-x)) = (-round(Rounding.down, x)))
  
  % Why3 of_real_post
  of_real_post(m:Rounding.mode, x:real, res:SingleFormat.single): bool =
    (value(res) = round(m, x)) AND ((exact(res) = x) AND (model(res) = x))
  
  % Why3 add_post
  add_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
    res:SingleFormat.single): bool = (value(res) = round(m,
    (value(x) + value(y)))) AND ((exact(res) = (exact(x) + exact(y))) AND
    (model(res) = (model(x) + model(y))))
  
  % Why3 sub_post
  sub_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
    res:SingleFormat.single): bool = (value(res) = round(m,
    (value(x) - value(y)))) AND ((exact(res) = (exact(x) - exact(y))) AND
    (model(res) = (model(x) - model(y))))
  
  % Why3 mul_post
  mul_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
    res:SingleFormat.single): bool = (value(res) = round(m,
    (value(x) * value(y)))) AND ((exact(res) = (exact(x) * exact(y))) AND
    (model(res) = (model(x) * model(y))))
  
  % Why3 div_post
  div_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
    res:SingleFormat.single): bool = (value(res) = round(m,
    real@Real.infix_sl(value(x), value(y)))) AND
    ((exact(res) = real@Real.infix_sl(exact(x), exact(y))) AND
    (model(res) = real@Real.infix_sl(model(x), model(y))))
  
  % Why3 neg_post
  neg_post(x:SingleFormat.single, res:SingleFormat.single): bool =
    (value(res) = (-value(x))) AND ((exact(res) = (-exact(x))) AND
    (model(res) = (-model(x))))
  
  % Why3 lt
  lt(x:SingleFormat.single, y:SingleFormat.single): bool =
    (value(x) <  value(y))
  
  % Why3 gt
  gt(x:SingleFormat.single, y:SingleFormat.single): bool =
    (value(x) >  value(y))
  
 END Single