tests/test-gappa2.why

   1
   2 theory T
   3
   4   use real.Real
   5   use real.Abs
   6   use floating_point.Rounding
   7   use floating_point.Double
   8
   9   constant a : double
  10   constant r : double
  11   function f int : double
  12
  13   lemma Test_eq1:
  14      value r = round NearestTiesToEven 0.1 ->
  15      a = r ->
  16      abs (value a - 0.1) <= 0x1.p-53
  17
  18   lemma Test_eq2:
  19      value r = round NearestTiesToEven 0.1 ->
  20      f 0 = r ->
  21      abs (value (f 0) - 0.1) <= 0x1.p-53
  22
  23 end