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-2015, 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 with 65 Post => (if X = 1.0 then Log'Result = 0.0); 66 67 function Log (X, Base : Float_Type'Base) return Float_Type'Base with 68 Post => (if X = 1.0 then Log'Result = 0.0); 69 70 function Exp (X : Float_Type'Base) return Float_Type'Base with 71 Post => (if X = 0.0 then Exp'Result = 1.0); 72 73 function "**" (Left, Right : Float_Type'Base) return Float_Type'Base with 74 Post => "**"'Result >= 0.0 75 and then (if Right = 0.0 then "**"'Result = 1.0) 76 and then (if Right = 1.0 then "**"'Result = Left) 77 and then (if Left = 1.0 then "**"'Result = 1.0) 78 and then (if Left = 0.0 then "**"'Result = 0.0); 79 80 function Sin (X : Float_Type'Base) return Float_Type'Base with 81 Post => Sin'Result in -1.0 .. 1.0 82 and then (if X = 0.0 then Sin'Result = 0.0); 83 84 function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with 85 Post => Sin'Result in -1.0 .. 1.0 86 and then (if X = 0.0 then Sin'Result = 0.0); 87 88 function Cos (X : Float_Type'Base) return Float_Type'Base with 89 Post => Cos'Result in -1.0 .. 1.0 90 and then (if X = 0.0 then Cos'Result = 1.0); 91 92 function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with 93 Post => Cos'Result in -1.0 .. 1.0 94 and then (if X = 0.0 then Cos'Result = 1.0); 95 96 function Tan (X : Float_Type'Base) return Float_Type'Base with 97 Post => (if X = 0.0 then Tan'Result = 0.0); 98 99 function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with 100 Post => (if X = 0.0 then Tan'Result = 0.0); 101 102 function Cot (X : Float_Type'Base) return Float_Type'Base; 103 104 function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base; 105 106 function Arcsin (X : Float_Type'Base) return Float_Type'Base with 107 Post => (if X = 0.0 then Arcsin'Result = 0.0); 108 109 function Arcsin (X, Cycle : Float_Type'Base) return Float_Type'Base with 110 Post => (if X = 0.0 then Arcsin'Result = 0.0); 111 112 function Arccos (X : Float_Type'Base) return Float_Type'Base with 113 Post => (if X = 1.0 then Arccos'Result = 0.0); 114 115 function Arccos (X, Cycle : Float_Type'Base) return Float_Type'Base with 116 Post => (if X = 1.0 then Arccos'Result = 0.0); 117 118 function Arctan 119 (Y : Float_Type'Base; 120 X : Float_Type'Base := 1.0) return Float_Type'Base 121 with 122 Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0); 123 124 function Arctan 125 (Y : Float_Type'Base; 126 X : Float_Type'Base := 1.0; 127 Cycle : Float_Type'Base) return Float_Type'Base 128 with 129 Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0); 130 131 function Arccot 132 (X : Float_Type'Base; 133 Y : Float_Type'Base := 1.0) return Float_Type'Base 134 with 135 Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0); 136 137 function Arccot 138 (X : Float_Type'Base; 139 Y : Float_Type'Base := 1.0; 140 Cycle : Float_Type'Base) return Float_Type'Base 141 with 142 Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0); 143 144 function Sinh (X : Float_Type'Base) return Float_Type'Base with 145 Post => (if X = 0.0 then Sinh'Result = 0.0); 146 147 function Cosh (X : Float_Type'Base) return Float_Type'Base with 148 Post => Cosh'Result >= 1.0 149 and then (if X = 0.0 then Cosh'Result = 1.0); 150 151 function Tanh (X : Float_Type'Base) return Float_Type'Base with 152 Post => Tanh'Result in -1.0 .. 1.0 153 and then (if X = 0.0 then Tanh'Result = 0.0); 154 155 function Coth (X : Float_Type'Base) return Float_Type'Base with 156 Post => abs Coth'Result >= 1.0; 157 158 function Arcsinh (X : Float_Type'Base) return Float_Type'Base with 159 Post => (if X = 0.0 then Arcsinh'Result = 0.0); 160 161 function Arccosh (X : Float_Type'Base) return Float_Type'Base with 162 Post => Arccosh'Result >= 0.0 163 and then (if X = 1.0 then Arccosh'Result = 0.0); 164 165 function Arctanh (X : Float_Type'Base) return Float_Type'Base with 166 Post => (if X = 0.0 then Arctanh'Result = 0.0); 167 168 function Arccoth (X : Float_Type'Base) return Float_Type'Base; 169 170end Ada.Numerics.Generic_Elementary_Functions; 171