Quelle  Diet.vdmpp   Sprache: VDM

\section{Diet Calculation}

\begin{vdm_al}
class Diet

values
public e = 1E-10;
public h = 1e-5; 

functions
static public BMI : real* real -> real
BMI(weight, height) ==
 let h100 = height / 100 in
 weight / h100 ** 2
pre
 weight > 0 and height > 0
post
 RESULT > 0;
\end{vdm_al}

\begin{vdm_al}
static public getWeightFromBMI : real * real -> real
getWeightFromBMI(height, aBMI) ==
 let 
  f = lambda weight : real & aBMI - BMI(weight, height) 
 in
 newton(f)(60)
pre
 height > 0 and aBMI > 0
post
 abs(aBMI - BMI(RESULT, height)) <= e;
\end{vdm_al}

\begin{vdm_al}
static public newton: (real ->real) -> real -> real
newton(f)(x) ==
 let isFinish = lambda y : real & abs(f(y)) < e,
  nextApproximate = lambda y : real & y - (f(y) / derivative(f)(y)) in
 Funtil[real](isFinish)(nextApproximate)(x);
\end{vdm_al}

\begin{vdm_al}
static public derivative : (real -> real) ->real -> real
derivative(f)(x) == (f(x+h) - f(x)) / h ;
\end{vdm_al}

\begin{vdm_al}
static public Funtil[@T] : (@T -> bool) -> (@T -> @T) -> @T -> @T
Funtil(p)(f)(x) == if p(x) then x else Funtil[@T](p)(f)(f(x));
\end{vdm_al}

\begin{vdm_al}
end Diet
\end{vdm_al}