x: double ( 0.0 <= x <= 1000.0);