Please read The Contract Guide at https://docs.racket-lang.org/guide/contracts.html?q=contracts
It has many examples and gradually builds intuition. The ideal PR would be to specific chapters there. > On May 4, 2017, at 12:38 AM, Daniel Prager <daniel.a.pra...@gmail.com> wrote: > > 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. -- 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.
