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