gcc/ada/a-ngelfu.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                ADA.NUMERICS.GENERIC_ELEMENTARY_FUNCTIONS                 --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --              Copyright (C) 2012, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- This specification is derived from the Ada Reference Manual for use with --
  12 -- GNAT. The copyright notice above, and the license provisions that follow --
  13 -- apply solely to the Post aspects that have been added to the spec.       --
  14 --                                                                          --
  15 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  16 -- terms of the  GNU General Public License as published  by the Free Soft- --
  17 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  18 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  19 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  20 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  21 --                                                                          --
  22 -- As a special exception under Section 7 of GPL version 3, you are granted --
  23 -- additional permissions described in the GCC Runtime Library Exception,   --
  24 -- version 3.1, as published by the Free Software Foundation.               --
  25 --                                                                          --
  26 -- You should have received a copy of the GNU General Public License and    --
  27 -- a copy of the GCC Runtime Library Exception along with this program;     --
  28 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  29 -- <http://www.gnu.org/licenses/>.                                          --
  30 --                                                                          --
  31 -- GNAT was originally developed  by the GNAT team at  New York University. --
  32 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  33 --                                                                          --
  34 ------------------------------------------------------------------------------
  35
  36 generic
  37    type Float_Type is digits <>;
  38
  39 package Ada.Numerics.Generic_Elementary_Functions is
  40    pragma Pure;
  41
  42    function Sqrt (X : Float_Type'Base) return Float_Type'Base
  43    with
  44      Post => Sqrt'Result >= 0.0
  45        and then (if X = 0.0 then Sqrt'Result = 0.0)
  46        and then (if X = 1.0 then Sqrt'Result = 1.0);
  47
  48    function Log (X : Float_Type'Base) return Float_Type'Base
  49    with
  50      Post => (if X = 1.0 then Log'Result = 0.0);
  51
  52    function Log (X, Base : Float_Type'Base) return Float_Type'Base
  53    with
  54      Post => (if X = 1.0 then Log'Result = 0.0);
  55
  56    function Exp (X : Float_Type'Base) return Float_Type'Base
  57    with
  58      Post => (if X = 0.0 then Exp'Result = 1.0);
  59
  60    function "**" (Left, Right : Float_Type'Base) return Float_Type'Base
  61    with
  62      Post => "**"'Result >= 0.0
  63        and then (if Right = 0.0 then "**"'Result = 1.0)
  64        and then (if Right = 1.0 then "**"'Result = Left)
  65        and then (if Left = 1.0 then "**"'Result = 1.0)
  66        and then (if Left = 0.0 then "**"'Result = 0.0);
  67
  68    function Sin (X : Float_Type'Base) return Float_Type'Base
  69    with
  70      Post => Sin'Result in -1.0 .. 1.0
  71        and then (if X = 0.0 then Sin'Result = 0.0);
  72
  73    function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base
  74    with
  75      Post => Sin'Result in -1.0 .. 1.0
  76        and then (if X = 0.0 then Sin'Result = 0.0);
  77
  78    function Cos (X : Float_Type'Base) return Float_Type'Base
  79    with
  80      Post => Cos'Result in -1.0 .. 1.0
  81        and then (if X = 0.0 then Cos'Result = 1.0);
  82
  83    function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base
  84    with
  85      Post => Cos'Result in -1.0 .. 1.0
  86        and then  (if X = 0.0 then Cos'Result = 1.0);
  87
  88    function Tan (X : Float_Type'Base) return Float_Type'Base
  89    with
  90      Post => (if X = 0.0 then Tan'Result = 0.0);
  91
  92    function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base
  93    with
  94      Post => (if X = 0.0 then Tan'Result = 0.0);
  95
  96    function Cot (X : Float_Type'Base) return Float_Type'Base;
  97
  98    function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base;
  99
 100    function Arcsin (X : Float_Type'Base) return Float_Type'Base
 101    with
 102      Post => (if X = 0.0 then Arcsin'Result = 0.0);
 103
 104    function Arcsin (X, Cycle : Float_Type'Base) return Float_Type'Base
 105    with
 106      Post => (if X = 0.0 then Arcsin'Result = 0.0);
 107
 108    function Arccos (X : Float_Type'Base) return Float_Type'Base
 109    with
 110      Post => (if X = 1.0 then Arccos'Result = 0.0);
 111
 112    function Arccos (X, Cycle : Float_Type'Base) return Float_Type'Base
 113    with
 114      Post => (if X = 1.0 then Arccos'Result = 0.0);
 115
 116    function Arctan
 117      (Y   : Float_Type'Base;
 118       X   : Float_Type'Base := 1.0)
 119      return Float_Type'Base
 120    with
 121      Post => (if X > 0.0 and Y = 0.0 then Arctan'Result = 0.0);
 122
 123    function Arctan
 124      (Y     : Float_Type'Base;
 125       X     : Float_Type'Base := 1.0;
 126       Cycle : Float_Type'Base)
 127       return  Float_Type'Base
 128    with
 129      Post => (if X > 0.0 and Y = 0.0 then Arctan'Result = 0.0);
 130
 131    function Arccot
 132      (X   : Float_Type'Base;
 133       Y   : Float_Type'Base := 1.0)
 134      return Float_Type'Base
 135    with
 136      Post => (if X > 0.0 and Y = 0.0 then Arccot'Result = 0.0);
 137
 138    function Arccot
 139      (X     : Float_Type'Base;
 140       Y     : Float_Type'Base := 1.0;
 141       Cycle : Float_Type'Base)
 142      return   Float_Type'Base
 143    with
 144      Post => (if X > 0.0 and Y = 0.0 then Arccot'Result = 0.0);
 145
 146    function Sinh (X : Float_Type'Base) return Float_Type'Base
 147    with
 148      Post => (if X = 0.0 then Sinh'Result = 0.0);
 149
 150    function Cosh (X : Float_Type'Base) return Float_Type'Base
 151    with
 152      Post => Cosh'Result >= 1.0
 153        and then (if X = 0.0 then Cosh'Result = 1.0);
 154
 155    function Tanh (X : Float_Type'Base) return Float_Type'Base
 156    with
 157      Post => Tanh'Result in -1.0 .. 1.0
 158        and then (if X = 0.0 then Tanh'Result = 0.0);
 159
 160    function Coth (X : Float_Type'Base) return Float_Type'Base
 161    with
 162      Post => abs Coth'Result >= 1.0;
 163
 164    function Arcsinh (X : Float_Type'Base) return Float_Type'Base
 165    with
 166      Post => (if X = 0.0 then Arcsinh'Result = 0.0);
 167
 168    function Arccosh (X : Float_Type'Base) return Float_Type'Base
 169    with
 170      Post => Arccosh'Result >= 0.0
 171        and then (if X = 1.0 then Arccosh'Result = 0.0);
 172
 173    function Arctanh (X : Float_Type'Base) return Float_Type'Base
 174    with
 175      Post => (if X = 0.0 then Arctanh'Result = 0.0);
 176
 177    function Arccoth (X : Float_Type'Base) return Float_Type'Base;
 178
 179 end Ada.Numerics.Generic_Elementary_Functions;