with Ada.Numerics.Elementary_Functions; use Ada.Numerics.Elementary_Functions;
with Safety_Pack; use Safety_Pack;
package body Maths_Pack
with SPARK_Mode
is
function Inv_Sqrt (X : Float) return Float is
function Sqrtf (X : Float) return Float with
Global => null,
Pre => X >= Float'Succ (0.0),
Post => Sqrtf'Result in 3.745E-23 .. 1.85E+19,
Import, Convention => C, External_Name => "sqrtf";
begin
return 1.0 / Sqrtf (X);
end Inv_Sqrt;
function Atan (Y : Float; X : Float) return T_Radians is
begin
-- We constrain the return value accordingly to
-- the Ada RM specification for Arctan
-- (A.5.1 Elementary Functions)
return Saturate (Arctan (Y, X), -Pi, Pi);
end Atan;
function Asin (X : Float) return T_Radians is
begin
-- We constrain the return value accordingly to
-- the Ada RM specification for Arcsin
-- (A.5.1 Elementary Functions)
return Saturate (Arcsin (X), -Pi / 2.0, Pi / 2.0);
end Asin;
end Maths_Pack;