init-F

Specification

?
\[\begin{array}{l} t_0 := D \cdot D - 1\\ t_1 := \sqrt{t\_0}\\ \mathbf{if}\;t\_0 \leq 0:\\ \;\;\;\;0\\ \mathbf{elif}\;phi0 < 0:\\ \;\;\;\;-t\_1\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \]
(FPCore (D phi0)
  :precision binary64
  :pre TRUE
  (let* ((t_0 (- (* D D) 1.0)) (t_1 (sqrt t_0)))
  (if (<= t_0 0.0) 0.0 (if (< phi0 0.0) (- t_1) t_1))))
double code(double D, double phi0) {
	double t_0 = (D * D) - 1.0;
	double t_1 = sqrt(t_0);
	double tmp;
	if (t_0 <= 0.0) {
		tmp = 0.0;
	} else if (phi0 < 0.0) {
		tmp = -t_1;
	} else {
		tmp = t_1;
	}
	return tmp;
}
real(8) function code(d, phi0)
use fmin_fmax_functions
    real(8), intent (in) :: d
    real(8), intent (in) :: phi0
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: tmp
    t_0 = (d * d) - 1.0d0
    t_1 = sqrt(t_0)
    if (t_0 <= 0.0d0) then
        tmp = 0.0d0
    else if (phi0 < 0.0d0) then
        tmp = -t_1
    else
        tmp = t_1
    end if
    code = tmp
end function
public static double code(double D, double phi0) {
	double t_0 = (D * D) - 1.0;
	double t_1 = Math.sqrt(t_0);
	double tmp;
	if (t_0 <= 0.0) {
		tmp = 0.0;
	} else if (phi0 < 0.0) {
		tmp = -t_1;
	} else {
		tmp = t_1;
	}
	return tmp;
}
def code(D, phi0):
	t_0 = (D * D) - 1.0
	t_1 = math.sqrt(t_0)
	tmp = 0
	if t_0 <= 0.0:
		tmp = 0.0
	elif phi0 < 0.0:
		tmp = -t_1
	else:
		tmp = t_1
	return tmp
function code(D, phi0)
	t_0 = Float64(Float64(D * D) - 1.0)
	t_1 = sqrt(t_0)
	tmp = 0.0
	if (t_0 <= 0.0)
		tmp = 0.0;
	elseif (phi0 < 0.0)
		tmp = Float64(-t_1);
	else
		tmp = t_1;
	end
	return tmp
end
function tmp_2 = code(D, phi0)
	t_0 = (D * D) - 1.0;
	t_1 = sqrt(t_0);
	tmp = 0.0;
	if (t_0 <= 0.0)
		tmp = 0.0;
	elseif (phi0 < 0.0)
		tmp = -t_1;
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end
code[D_, phi0_] := Block[{t$95$0 = N[(N[(D * D), $MachinePrecision] - 1.0), $MachinePrecision]}, Block[{t$95$1 = N[Sqrt[t$95$0], $MachinePrecision]}, If[LessEqual[t$95$0, 0.0], 0.0, If[Less[phi0, 0.0], (-t$95$1), t$95$1]]]]
f(D, phi0):
	D in [-inf, +inf],
	phi0 in [-inf, +inf]
code: THEORY
BEGIN
f(D, phi0: real): real =
	LET t_0 = ((D * D) - (1)) IN
		LET t_1 = (sqrt(t_0)) IN
			LET tmp_1 = IF (phi0 < (0)) THEN (- t_1) ELSE t_1 ENDIF IN
			LET tmp = IF (t_0 <= (0)) THEN (0) ELSE tmp_1 ENDIF IN
	tmp
END code
\begin{array}{l}
t_0 := D \cdot D - 1\\
t_1 := \sqrt{t\_0}\\
\mathbf{if}\;t\_0 \leq 0:\\
\;\;\;\;0\\

\mathbf{elif}\;phi0 < 0:\\
\;\;\;\;-t\_1\\

\mathbf{else}:\\
\;\;\;\;t\_1\\


\end{array}

Timeout after 2.5min

Use the --timeout flag to change the timeout.