For example, the library Cofoja for Java offers the following options:

@Requires("x >= 0")
@Ensures("result >= 0")
static double sqrt(double x);

This would ensure that the function sqrt could be called up only with a non-negative argument. However, this specification does not show that the square of result again corresponds to x (or is within the rounding error).