1 ------------------------------------------------------------------------------
3 -- GNAT RUN-TIME COMPONENTS --
5 -- ADA.NUMERICS.GENERIC_ELEMENTARY_FUNCTIONS --
9 -- Copyright (C) 2012-2017, Free Software Foundation, Inc. --
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. --
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. --
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. --
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/>. --
31 -- GNAT was originally developed by the GNAT team at New York University. --
32 -- Extensive contributions were provided by Ada Core Technologies Inc. --
34 ------------------------------------------------------------------------------
37 type Float_Type
is digits <>;
39 package Ada
.Numerics
.Generic_Elementary_Functions
with
44 -- Preconditions in this unit are meant for analysis only, not for run-time
45 -- checking, so that the expected exceptions are raised when calling
46 -- Assert. This is enforced by setting the corresponding assertion policy
47 -- to Ignore. This is done in the generic spec so that it applies to all
50 pragma Assertion_Policy
(Pre
=> Ignore
);
52 function Sqrt
(X
: Float_Type
'Base) return Float_Type
'Base with
54 Post
=> Sqrt
'Result >= 0.0
55 and then (if X
= 0.0 then Sqrt
'Result = 0.0)
56 and then (if X
= 1.0 then Sqrt
'Result = 1.0)
58 -- Finally if X is positive, the result of Sqrt is positive (because
59 -- the sqrt of numbers greater than 1 is greater than or equal to 1,
60 -- and the sqrt of numbers less than 1 is greater than the argument).
62 -- This property is useful in particular for static analysis. The
63 -- property that X is positive is not expressed as (X > 0.0), as
64 -- the value X may be held in registers that have larger range and
65 -- precision on some architecture (for example, on x86 using x387
66 -- FPU, as opposed to SSE2). So, it might be possible for X to be
67 -- 2.0**(-5000) or so, which could cause the number to compare as
68 -- greater than 0, but Sqrt would still return a zero result.
70 -- Note: we use the comparison with Succ (0.0) here because this is
71 -- more amenable to CodePeer analysis than the use of 'Machine.
73 and then (if X
>= Float_Type
'Succ (0.0) then Sqrt
'Result > 0.0);
75 function Log
(X
: Float_Type
'Base) return Float_Type
'Base with
77 Post
=> (if X
= 1.0 then Log
'Result = 0.0);
79 function Log
(X
, Base
: Float_Type
'Base) return Float_Type
'Base with
80 Pre
=> X
> 0.0 and Base
> 0.0 and Base
/= 1.0,
81 Post
=> (if X
= 1.0 then Log
'Result = 0.0);
83 function Exp
(X
: Float_Type
'Base) return Float_Type
'Base with
84 Post
=> (if X
= 0.0 then Exp
'Result = 1.0);
86 function "**" (Left
, Right
: Float_Type
'Base) return Float_Type
'Base with
87 Pre
=> (if Left
= 0.0 then Right
> 0.0) and Left
>= 0.0,
88 Post
=> "**"'Result >= 0.0
89 and then (if Right = 0.0 then "**"'Result
= 1.0)
90 and then (if Right
= 1.0 then "**"'Result = Left)
91 and then (if Left = 1.0 then "**"'Result
= 1.0)
92 and then (if Left
= 0.0 then "**"'Result = 0.0);
94 function Sin (X : Float_Type'Base) return Float_Type'Base with
95 Post => Sin'Result in -1.0 .. 1.0
96 and then (if X = 0.0 then Sin'Result = 0.0);
98 function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with
100 Post => Sin'Result in -1.0 .. 1.0
101 and then (if X = 0.0 then Sin'Result = 0.0);
103 function Cos (X : Float_Type'Base) return Float_Type'Base with
104 Post => Cos'Result in -1.0 .. 1.0
105 and then (if X = 0.0 then Cos'Result = 1.0);
107 function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with
109 Post => Cos'Result in -1.0 .. 1.0
110 and then (if X = 0.0 then Cos'Result = 1.0);
112 function Tan (X : Float_Type'Base) return Float_Type'Base with
113 Post => (if X = 0.0 then Tan'Result = 0.0);
115 function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with
117 and then abs Float_Type'Base'Remainder
(X
, Cycle
) /= 0.25 * Cycle
,
118 Post
=> (if X
= 0.0 then Tan
'Result = 0.0);
120 function Cot
(X
: Float_Type
'Base) return Float_Type
'Base with
123 function Cot
(X
, Cycle
: Float_Type
'Base) return Float_Type
'Base with
126 and then Float_Type
'Base'Remainder (X, Cycle) /= 0.0
127 and then abs Float_Type'Base'Remainder
(X
, Cycle
) = 0.5 * Cycle
;
129 function Arcsin
(X
: Float_Type
'Base) return Float_Type
'Base with
131 Post
=> (if X
= 0.0 then Arcsin
'Result = 0.0);
133 function Arcsin
(X
, Cycle
: Float_Type
'Base) return Float_Type
'Base with
134 Pre
=> Cycle
> 0.0 and abs X
<= 1.0,
135 Post
=> (if X
= 0.0 then Arcsin
'Result = 0.0);
137 function Arccos
(X
: Float_Type
'Base) return Float_Type
'Base with
139 Post
=> (if X
= 1.0 then Arccos
'Result = 0.0);
141 function Arccos
(X
, Cycle
: Float_Type
'Base) return Float_Type
'Base with
142 Pre
=> Cycle
> 0.0 and abs X
<= 1.0,
143 Post
=> (if X
= 1.0 then Arccos
'Result = 0.0);
146 (Y
: Float_Type
'Base;
147 X
: Float_Type
'Base := 1.0) return Float_Type
'Base
149 Pre
=> X
/= 0.0 or Y
/= 0.0,
150 Post
=> (if X
> 0.0 and then Y
= 0.0 then Arctan
'Result = 0.0);
153 (Y
: Float_Type
'Base;
154 X
: Float_Type
'Base := 1.0;
155 Cycle
: Float_Type
'Base) return Float_Type
'Base
157 Pre
=> Cycle
> 0.0 and (X
/= 0.0 or Y
/= 0.0),
158 Post
=> (if X
> 0.0 and then Y
= 0.0 then Arctan
'Result = 0.0);
161 (X
: Float_Type
'Base;
162 Y
: Float_Type
'Base := 1.0) return Float_Type
'Base
164 Pre
=> X
/= 0.0 or Y
/= 0.0,
165 Post
=> (if X
> 0.0 and then Y
= 0.0 then Arccot
'Result = 0.0);
168 (X
: Float_Type
'Base;
169 Y
: Float_Type
'Base := 1.0;
170 Cycle
: Float_Type
'Base) return Float_Type
'Base
172 Pre
=> Cycle
> 0.0 and (X
/= 0.0 or Y
/= 0.0),
173 Post
=> (if X
> 0.0 and then Y
= 0.0 then Arccot
'Result = 0.0);
175 function Sinh
(X
: Float_Type
'Base) return Float_Type
'Base with
176 Post
=> (if X
= 0.0 then Sinh
'Result = 0.0);
178 function Cosh
(X
: Float_Type
'Base) return Float_Type
'Base with
179 Post
=> Cosh
'Result >= 1.0
180 and then (if X
= 0.0 then Cosh
'Result = 1.0);
182 function Tanh
(X
: Float_Type
'Base) return Float_Type
'Base with
183 Post
=> Tanh
'Result in -1.0 .. 1.0
184 and then (if X
= 0.0 then Tanh
'Result = 0.0);
186 function Coth
(X
: Float_Type
'Base) return Float_Type
'Base with
188 Post
=> abs Coth
'Result >= 1.0;
190 function Arcsinh
(X
: Float_Type
'Base) return Float_Type
'Base with
191 Post
=> (if X
= 0.0 then Arcsinh
'Result = 0.0);
193 function Arccosh
(X
: Float_Type
'Base) return Float_Type
'Base with
195 Post
=> Arccosh
'Result >= 0.0
196 and then (if X
= 1.0 then Arccosh
'Result = 0.0);
198 function Arctanh
(X
: Float_Type
'Base) return Float_Type
'Base with
200 Post
=> (if X
= 0.0 then Arctanh
'Result = 0.0);
202 function Arccoth
(X
: Float_Type
'Base) return Float_Type
'Base with
203 Pre
=> X
<= 1.0 and abs X
/= 1.0;
205 end Ada
.Numerics
.Generic_Elementary_Functions
;