`sqrt(x) < x` not a valid check

[CrossEye]

In examples/dependent.js, we have this contract for a supposed square root function:

@ (x: Pos) -> res: Num | res <= x

And the failing implementation of sqrt is

return x * x;

Both of these have some issues in the range (0, 1). Note that sqrt(0.25); //=> 0.5 and that 0.5 < 0.25; //=> false. Similarly, in the same range 0.7 * 0,7 = 0.49, and 0.49 < 0.7, so this succeeds for range (0, 1).

I'm brand-new here, and don't know if this is acceptable. Obviously, any value that makes such a contract fail is a demonstration that the implementation is wrong, but I don't know what standard you want to set with the examples.

[disnet]

Ha, good catch. That contract is definitely not what we want to say.

Maybe something like this is better.

@ (x: Pos) -> res:Num | res > (Math.sqrt(x) - 0.1) &&
                        res < (Math.sqrt(x) + 0.1)

Thanks for letting me know!

[CrossEye]

I would suggest that, since a sqrt function is what you're trying to define, using another one in its contract is perhaps a little odd. Is a syntax like this acceptable?:

@ (x: Pos) -> res:Num | (res * res + 0.1) > x && (res * res - 0.1) < x

[disnet]

Good call, that's probably a bit more clear.