Using Ben's left-pad example as a model I get the following re-write of the
real-sqrt contract
(([x real?])
#:pre/name (x)
"non-negative argument expected"
(>= x 0)
. ->i .
[result (x) real?]
#:post/name (x result)
"the sqrt of zero is zero"
(implies (= x 0) (= result 0))
#:post/name (x result)
"the sqrt of a positive number is positive"
(implies (> x 0) (> result 0))
#:post/name (x result)
"result * result = x (to within error)"
(implies (> x 0) (<= (abs (- x (* result result))) 0.00000001)))
Other than a bit of repetition — multiple uses of #:post/name — this is
pretty darn close to what I was after.
Like most people, when faced with something complex and a bit daunting — in
this case the ->i contract combinator — I benefit from concrete examples.
If enough people encourage me to "make a pull request" once I'm more
familiar I'll propose some more examples myself.
* * *
My off-hand proposal would be to permit a variation on #:pre/name,
#:post/name and friends to allow multiple clauses. For example:
#:post/name (x result)
["sqrt of zero is zero" (implies (= x 0) (= result 0))]
["sqrt of a positive number is positive" (implies (> x 0) (> result 0))]
["result * result = x (to within error)"
(implies (> x 0) (<= (abs (- x (* result result))) 0.00000001))]
Next stop ... boundaries.
Thanks again
Dan
On Wed, May 3, 2017 at 1:57 PM, Ben Greenman <benjaminlgreen...@gmail.com>
wrote:
1. To practice with dependent contracts, I made a "full" spec for the
> JavaScript left-pad function.
> https://www.npmjs.com/package/left-pad
>
> The exercise was fun, I learned a lot, and I think my solution is "as
> readable as possible" :) .
> https://github.com/bennn/racket-left-pad
>
>
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
