double f(double x) 
  \requires x > 0;
  \ensures \true;
  ;

double g(double x)
  \requires x > 0;
  \ensures \result >= 0;
{
  return g(x)*g(x);
}

double main() {
  return g(2);
}