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