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-2019, 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 36generic 37 type Float_Type is digits <>; 38 39package Ada.Numerics.Generic_Elementary_Functions with 40 SPARK_Mode => On 41is 42 pragma Pure; 43 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 48 -- instances. 49 50 pragma Assertion_Policy (Pre => Ignore); 51 52 function Sqrt (X : Float_Type'Base) return Float_Type'Base with 53 Pre => X >= 0.0, 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) 57 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). 61 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. 69 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. 72 73 and then (if X >= Float_Type'Succ (0.0) then Sqrt'Result > 0.0); 74 75 function Log (X : Float_Type'Base) return Float_Type'Base with 76 Pre => X > 0.0, 77 Post => (if X = 1.0 then Log'Result = 0.0); 78 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); 82 83 function Exp (X : Float_Type'Base) return Float_Type'Base with 84 Post => (if X = 0.0 then Exp'Result = 1.0); 85 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); 93 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); 97 98 function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with 99 Pre => Cycle > 0.0, 100 Post => Sin'Result in -1.0 .. 1.0 101 and then (if X = 0.0 then Sin'Result = 0.0); 102 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); 106 107 function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with 108 Pre => Cycle > 0.0, 109 Post => Cos'Result in -1.0 .. 1.0 110 and then (if X = 0.0 then Cos'Result = 1.0); 111 112 function Tan (X : Float_Type'Base) return Float_Type'Base with 113 Post => (if X = 0.0 then Tan'Result = 0.0); 114 115 function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with 116 Pre => Cycle > 0.0 117 and then abs Float_Type'Base'Remainder (X, Cycle) /= 0.25 * Cycle, 118 Post => (if X = 0.0 then Tan'Result = 0.0); 119 120 function Cot (X : Float_Type'Base) return Float_Type'Base with 121 Pre => X /= 0.0; 122 123 function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base with 124 Pre => Cycle > 0.0 125 and then X /= 0.0 126 and then Float_Type'Base'Remainder (X, Cycle) /= 0.0 127 and then abs Float_Type'Base'Remainder (X, Cycle) = 0.5 * Cycle; 128 129 function Arcsin (X : Float_Type'Base) return Float_Type'Base with 130 Pre => abs X <= 1.0, 131 Post => (if X = 0.0 then Arcsin'Result = 0.0); 132 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); 136 137 function Arccos (X : Float_Type'Base) return Float_Type'Base with 138 Pre => abs X <= 1.0, 139 Post => (if X = 1.0 then Arccos'Result = 0.0); 140 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); 144 145 function Arctan 146 (Y : Float_Type'Base; 147 X : Float_Type'Base := 1.0) return Float_Type'Base 148 with 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); 151 152 function Arctan 153 (Y : Float_Type'Base; 154 X : Float_Type'Base := 1.0; 155 Cycle : Float_Type'Base) return Float_Type'Base 156 with 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); 159 160 function Arccot 161 (X : Float_Type'Base; 162 Y : Float_Type'Base := 1.0) return Float_Type'Base 163 with 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); 166 167 function Arccot 168 (X : Float_Type'Base; 169 Y : Float_Type'Base := 1.0; 170 Cycle : Float_Type'Base) return Float_Type'Base 171 with 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); 174 175 function Sinh (X : Float_Type'Base) return Float_Type'Base with 176 Post => (if X = 0.0 then Sinh'Result = 0.0); 177 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); 181 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); 185 186 function Coth (X : Float_Type'Base) return Float_Type'Base with 187 Pre => X /= 0.0, 188 Post => abs Coth'Result >= 1.0; 189 190 function Arcsinh (X : Float_Type'Base) return Float_Type'Base with 191 Post => (if X = 0.0 then Arcsinh'Result = 0.0); 192 193 function Arccosh (X : Float_Type'Base) return Float_Type'Base with 194 Pre => X >= 1.0, 195 Post => Arccosh'Result >= 0.0 196 and then (if X = 1.0 then Arccosh'Result = 0.0); 197 198 function Arctanh (X : Float_Type'Base) return Float_Type'Base with 199 Pre => abs X < 1.0, 200 Post => (if X = 0.0 then Arctanh'Result = 0.0); 201 202 function Arccoth (X : Float_Type'Base) return Float_Type'Base with 203 Pre => abs X > 1.0; 204 205end Ada.Numerics.Generic_Elementary_Functions; 206