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-2014, 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 is 40 pragma Pure; 41 42 function Sqrt (X : Float_Type'Base) return Float_Type'Base with 43 Post => Sqrt'Result >= 0.0 44 and then (if X = 0.0 then Sqrt'Result = 0.0) 45 and then (if X = 1.0 then Sqrt'Result = 1.0) 46 47 -- Finally if X is positive, the result of Sqrt is positive (because 48 -- the sqrt of numbers greater than 1 is greater than or equal to 1, 49 -- and the sqrt of numbers less than 1 is greater than the argument). 50 51 -- This property is useful in particular for static analysis. The 52 -- property that X is positive is not expressed as (X > 0.0), as 53 -- the value X may be held in registers that have larger range and 54 -- precision on some architecture (for example, on x86 using x387 55 -- FPU, as opposed to SSE2). So, it might be possible for X to be 56 -- 2.0**(-5000) or so, which could cause the number to compare as 57 -- greater than 0, but Sqrt would still return a zero result. 58 59 -- Note: we use the comparison with Succ (0.0) here because this is 60 -- more amenable to CodePeer analysis than the use of 'Machine. 61 62 and then (if X >= Float_Type'Succ (0.0) then Sqrt'Result > 0.0); 63 64 function Log (X : Float_Type'Base) return Float_Type'Base 65 with 66 Post => (if X = 1.0 then Log'Result = 0.0); 67 68 function Log (X, Base : Float_Type'Base) return Float_Type'Base with 69 Post => (if X = 1.0 then Log'Result = 0.0); 70 71 function Exp (X : Float_Type'Base) return Float_Type'Base with 72 Post => (if X = 0.0 then Exp'Result = 1.0); 73 74 function "**" (Left, Right : Float_Type'Base) return Float_Type'Base with 75 Post => "**"'Result >= 0.0 76 and then (if Right = 0.0 then "**"'Result = 1.0) 77 and then (if Right = 1.0 then "**"'Result = Left) 78 and then (if Left = 1.0 then "**"'Result = 1.0) 79 and then (if Left = 0.0 then "**"'Result = 0.0); 80 81 function Sin (X : Float_Type'Base) return Float_Type'Base with 82 Post => Sin'Result in -1.0 .. 1.0 83 and then (if X = 0.0 then Sin'Result = 0.0); 84 85 function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with 86 Post => Sin'Result in -1.0 .. 1.0 87 and then (if X = 0.0 then Sin'Result = 0.0); 88 89 function Cos (X : Float_Type'Base) return Float_Type'Base with 90 Post => Cos'Result in -1.0 .. 1.0 91 and then (if X = 0.0 then Cos'Result = 1.0); 92 93 function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with 94 Post => Cos'Result in -1.0 .. 1.0 95 and then (if X = 0.0 then Cos'Result = 1.0); 96 97 function Tan (X : Float_Type'Base) return Float_Type'Base with 98 Post => (if X = 0.0 then Tan'Result = 0.0); 99 100 function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with 101 Post => (if X = 0.0 then Tan'Result = 0.0); 102 103 function Cot (X : Float_Type'Base) return Float_Type'Base; 104 105 function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base; 106 107 function Arcsin (X : Float_Type'Base) return Float_Type'Base with 108 Post => (if X = 0.0 then Arcsin'Result = 0.0); 109 110 function Arcsin (X, Cycle : Float_Type'Base) return Float_Type'Base with 111 Post => (if X = 0.0 then Arcsin'Result = 0.0); 112 113 function Arccos (X : Float_Type'Base) return Float_Type'Base with 114 Post => (if X = 1.0 then Arccos'Result = 0.0); 115 116 function Arccos (X, Cycle : Float_Type'Base) return Float_Type'Base with 117 Post => (if X = 1.0 then Arccos'Result = 0.0); 118 119 function Arctan 120 (Y : Float_Type'Base; 121 X : Float_Type'Base := 1.0) return Float_Type'Base 122 with 123 Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0); 124 125 function Arctan 126 (Y : Float_Type'Base; 127 X : Float_Type'Base := 1.0; 128 Cycle : Float_Type'Base) return Float_Type'Base 129 with 130 Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0); 131 132 function Arccot 133 (X : Float_Type'Base; 134 Y : Float_Type'Base := 1.0) return Float_Type'Base 135 with 136 Post => (if X > 0.0 and then 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) return Float_Type'Base 142 with 143 Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0); 144 145 function Sinh (X : Float_Type'Base) return Float_Type'Base with 146 Post => (if X = 0.0 then Sinh'Result = 0.0); 147 148 function Cosh (X : Float_Type'Base) return Float_Type'Base with 149 Post => Cosh'Result >= 1.0 150 and then (if X = 0.0 then Cosh'Result = 1.0); 151 152 function Tanh (X : Float_Type'Base) return Float_Type'Base with 153 Post => Tanh'Result in -1.0 .. 1.0 154 and then (if X = 0.0 then Tanh'Result = 0.0); 155 156 function Coth (X : Float_Type'Base) return Float_Type'Base with 157 Post => abs Coth'Result >= 1.0; 158 159 function Arcsinh (X : Float_Type'Base) return Float_Type'Base with 160 Post => (if X = 0.0 then Arcsinh'Result = 0.0); 161 162 function Arccosh (X : Float_Type'Base) return Float_Type'Base with 163 Post => Arccosh'Result >= 0.0 164 and then (if X = 1.0 then Arccosh'Result = 0.0); 165 166 function Arctanh (X : Float_Type'Base) return Float_Type'Base with 167 Post => (if X = 0.0 then Arctanh'Result = 0.0); 168 169 function Arccoth (X : Float_Type'Base) return Float_Type'Base; 170 171end Ada.Numerics.Generic_Elementary_Functions; 172