File : a-ngelfu-ada.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT RUNTIME COMPONENTS --
4 -- --
5 -- ADA.NUMERICS.GENERIC_ELEMENTARY_FUNCTIONS --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. --
17 -- --
18 -- --
19 -- --
20 -- --
21 -- --
22 -- You should have received a copy of the GNU General Public License and --
23 -- a copy of the GCC Runtime Library Exception along with this program; --
24 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
25 -- <http://www.gnu.org/licenses/>. --
26 -- --
27 -- GNAT was originally developed by the GNAT team at New York University. --
28 -- Extensive contributions were provided by Ada Core Technologies Inc. --
29 -- --
30 ------------------------------------------------------------------------------
31
32 -- @llrset a-ngelfu.ads
33 -- Generic_Elementary_Functions
34 -- ============================
35
36 -- This is the Ada Cert Math version of a-ngelfu.ads
37
38 generic
39 type Float_Type is digits <>;
40
41 package Ada.Numerics.Generic_Elementary_Functions is
42 pragma Pure (Generic_Elementary_Functions);
43
44 function Sqrt (X : Float_Type'Base) return Float_Type'Base with
45 -- @llr Sqrt (Float_Type)
46 -- This function shall return the square root of <X>.
47 Post => Sqrt'Result >= 0.0
48 and then (if X = 0.0 then Sqrt'Result = 0.0)
49 and then (if X = 1.0 then Sqrt'Result = 1.0)
50
51 -- Finally if X is positive, the result of Sqrt is positive (because
52 -- the sqrt of numbers greater than 1 is greater than or equal to 1,
53 -- and the sqrt of numbers less than 1 is greater than the argument).
54
55 -- This property is useful in particular for static analysis. The
56 -- property that X is positive is not expressed as (X > 0.0), as
57 -- the value X may be held in registers that have larger range and
58 -- precision on some architecture (for example, on x86 using x387
59 -- FPU, as opposed to SSE2). So, it might be possible for X to be
60 -- 2.0**(-5000) or so, which could cause the number to compare as
61 -- greater than 0, but Sqrt would still return a zero result.
62
63 -- Note: we use the comparison with Succ (0.0) here because this is
64 -- more amenable to CodePeer analysis than the use of 'Machine.
65
66 and then (if X >= Float_Type'Succ (0.0) then Sqrt'Result > 0.0);
67
68 function Log (X : Float_Type'Base) return Float_Type'Base with
69 -- @llr Log (Float_Type)
70 -- This function shall return the logarithm of <X>.
71 Post => (if X = 1.0 then Log'Result = 0.0);
72
73 function Log (X, Base : Float_Type'Base) return Float_Type'Base with
74 -- @llr Log (Float_Type; Float_Type)
75 -- This function shall compute the logarithm of <X> with the specified
76 -- base.
77 Post => (if X = 1.0 then Log'Result = 0.0);
78
79 function Exp (X : Float_Type'Base) return Float_Type'Base with
80 -- @llr Exp (Float_Type)
81 -- This function shall compute the exponent of <X>.
82 Post => (if X = 0.0 then Exp'Result = 1.0);
83
84 function "**" (Left, Right : Float_Type'Base) return Float_Type'Base with
85 -- @llr "**" (Float_Type; Float_Type)
86 -- This function shall compute <Left> to the power of <Right>.
87 Post => "**"'Result >= 0.0
88 and then (if Right = 0.0 then "**"'Result = 1.0)
89 and then (if Right = 1.0 then "**"'Result = Left)
90 and then (if Left = 1.0 then "**"'Result = 1.0)
91 and then (if Left = 0.0 then "**"'Result = 0.0);
92
93 function Sin (X : Float_Type'Base) return Float_Type'Base with
94 -- @llr Sin (Float_Type)
95 -- This function shall return the sine of <X>.
96 Post => Sin'Result in -1.0 .. 1.0
97 and then (if X = 0.0 then Sin'Result = 0.0);
98
99 function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with
100 -- @llr Sin (Float_Type; Float_Type)
101 -- This function shall return the sine of <X> with the specified base.
102 Post => Sin'Result in -1.0 .. 1.0
103 and then (if X = 0.0 then Sin'Result = 0.0);
104
105 function Cos (X : Float_Type'Base) return Float_Type'Base with
106 -- @llr Cos (Float_Type)
107 -- This function shall return the cosine of <X>.
108 Post => Cos'Result in -1.0 .. 1.0
109 and then (if X = 0.0 then Cos'Result = 1.0);
110
111 function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with
112 -- @llr Cos (Float_Type; Float_Type)
113 -- This funtion shall return the cosine of <X> with the sepcified base.
114 Post => Cos'Result in -1.0 .. 1.0
115 and then (if X = 0.0 then Cos'Result = 1.0);
116
117 function Tan (X : Float_Type'Base) return Float_Type'Base with
118 -- @llr Tan (Float_Type)
119 -- This function shall return the tangent of <X>.
120 Post => (if X = 0.0 then Tan'Result = 0.0);
121
122 function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with
123 -- @llr Tan (Float_Type; Float_Type)
124 -- This funtion shall return the tangent of <X> with the sepcified base.
125 Post => (if X = 0.0 then Tan'Result = 0.0);
126
127 function Cot (X : Float_Type'Base) return Float_Type'Base;
128 -- @llr Cot (Float_Type)
129 -- This function shall return the cotangent of <X>.
130
131 function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base;
132 -- @llr Cot (Float_Type; Float_Type)
133 -- This funtion shall return the cotangent of <X> with the sepcified base.
134
135 function Arcsin (X : Float_Type'Base) return Float_Type'Base with
136 -- @llr Arcsin (Float_Type)
137 -- This function shall return the inverse sine of <X>.
138 Post => (if X = 0.0 then Arcsin'Result = 0.0);
139
140 function Arcsin (X, Cycle : Float_Type'Base) return Float_Type'Base with
141 -- @llr Arcsin (Float_Type; Float_Type)
142 -- This funtion shall return the inverse sine of <X> with the specified
143 -- base.
144 Post => (if X = 0.0 then Arcsin'Result = 0.0);
145
146 function Arccos (X : Float_Type'Base) return Float_Type'Base with
147 -- @llr Arccos (Float_Type)
148 -- This function shall return the inverse cosine of <X>.
149 Post => (if X = 1.0 then Arccos'Result = 0.0);
150
151 function Arccos (X, Cycle : Float_Type'Base) return Float_Type'Base with
152 -- @llr Arccos (Float_Type; Float_Type)
153 -- This funtion shall return the inverse cosine of <X> with the specified
154 -- base.
155 Post => (if X = 1.0 then Arccos'Result = 0.0);
156
157 function Arctan
158 (Y : Float_Type'Base;
159 X : Float_Type'Base := 1.0) return Float_Type'Base with
160 -- @llr Arctan (Float_Type; Float_Type)
161 -- This function shall compute the principal value of the inverse tangent
162 -- of <Y> / <X>.
163 Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0);
164
165 function Arctan
166 (Y : Float_Type'Base;
167 X : Float_Type'Base := 1.0;
168 Cycle : Float_Type'Base) return Float_Type'Base with
169 -- @llr Arctan (Float_Type; Float_Type; FLoat_Type)
170 -- This function shall compute the principal value of the inverse tangent
171 -- of <Y> / <X> with the specified base.
172 Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0);
173
174 function Arccot
175 (X : Float_Type'Base;
176 Y : Float_Type'Base := 1.0) return Float_Type'Base with
177 -- @llr Arccot (Float_Type; Float_Type)
178 -- This function shall compute the principal value of the inverse cotangent
179 -- of <Y> / <X>.
180 Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
181
182 function Arccot
183 (X : Float_Type'Base;
184 Y : Float_Type'Base := 1.0;
185 Cycle : Float_Type'Base) return Float_Type'Base with
186 -- @llr Arccot (Float_Type; Float_Type; FLoat_Type)
187 -- This function shall compute the principal value of the inverse cotangent
188 -- of <Y> / <X> with the specified base.
189 Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
190
191 function Sinh (X : Float_Type'Base) return Float_Type'Base with
192 -- @llr Sinh (Float_Type)
193 -- This function shall return the hyperbolic sine of <X>.
194 Post => (if X = 0.0 then Sinh'Result = 0.0);
195
196 function Cosh (X : Float_Type'Base) return Float_Type'Base with
197 -- @llr Cosh (Float_Type)
198 -- This function shall return the hyperbolic cosine of <X>.
199 Post => Cosh'Result >= 1.0
200 and then (if X = 0.0 then Cosh'Result = 1.0);
201
202 function Tanh (X : Float_Type'Base) return Float_Type'Base with
203 -- @llr Tanh (Float_Type)
204 -- This function shall return the hyperbolic tangent of <X>.
205 Post => Tanh'Result in -1.0 .. 1.0
206 and then (if X = 0.0 then Tanh'Result = 0.0);
207
208 function Coth (X : Float_Type'Base) return Float_Type'Base with
209 -- @llr Coth (Float_Type)
210 -- This function shall return the hyperbolic cotangent of <X>.
211 Post => abs Coth'Result >= 1.0;
212
213 function Arcsinh (X : Float_Type'Base) return Float_Type'Base with
214 -- @llr Arcsinh (Float_Type)
215 -- This function shall return the inverse hyperbolic sine of <X>.
216 Post => (if X = 0.0 then Arcsinh'Result = 0.0);
217
218 function Arccosh (X : Float_Type'Base) return Float_Type'Base with
219 -- @llr Arccosh (Float_Type)
220 -- This function shall return the inverse hyperbolic cosine of <X>.
221 Post => Arccosh'Result >= 0.0
222 and then (if X = 1.0 then Arccosh'Result = 0.0);
223
224 function Arctanh (X : Float_Type'Base) return Float_Type'Base with
225 -- @llr Arctanh (Float_Type)
226 -- This function shall return the inverse hyperbolic tangent of <X>.
227 Post => (if X = 0.0 then Arctanh'Result = 0.0);
228
229 function Arccoth (X : Float_Type'Base) return Float_Type'Base;
230 -- @llr Arccoth (Float_Type)
231 -- This function shall return the inverse hyperbolic cotangent of <X>.
232
233 private
234 pragma Assert
235 (Float_Type'Machine_Radix = 2,
236 "only binary floating-point types supported");
237 -- Why not Compile_Time_Error??? here
238 end Ada.Numerics.Generic_Elementary_Functions;