> On May 2, 2017, at 4:33 PM, Daniel Prager <daniel.a.pra...@gmail.com> wrote:
>
> (define/pre-post (real-sqrt x)
> #:pre ([(real? x) "real argument expected"]
> [(>= x 0) "non-negative argument expected"])
>
> #:implementation (sqrt x)
>
> #:post ([(implies (= x 0) (= result 0)) "The sqrt of zero should be zero"]
> [(implies (> x 0) (> result 0)) "Positive numbers have positive
> square-roots"]
> [(implies (> x 0) (<= (abs (- x (* result result))) 0.0000001))
> "result * result = x (to within error)"]))
It sounds like you want alternate notation for stuff the contract system can
already do.
AFAICT the function below is equivalent to your function above. One could
create a macro to go from one to the other:
(define/contract (real-sqrt x)
(([x (and/c
(or/c (λ (x) (real? x))
(curry raise-argument-error 'real-sqrt "real argument expected"))
(or/c (λ (x) (>= x 0))
(curry raise-argument-error 'real-sqrt "non-negative argument
expected")))])
. ->i .
[result (x)
(cond
[(= x 0) (or/c (λ (result) (= result 0))
(curry raise-result-error 'real-sqrt "sqrt of zero
should be zero"))]
[(> x 0) (and/c
(or/c (λ (result) (> result 0))
(curry raise-result-error 'real-sqrt "sqrt
of positive number should be positive"))
(or/c (λ (result) (<= (abs (- x (* result
result))) 0.00000001))
(curry raise-result-error 'real-sqrt
"result * result = x (to within error)")))])])
(sqrt x))
> Thinking more about the functional context, a macro — say (define/pre-post
> ...) that cleanly defined the following functions would be pretty sweet
> (continuing with the real-sqrt example):
> real-sqrt-unsafe
> real-sqrt-with-pre-conditions
> real-sqrt-with-pre-and-post-conditions
> real-sqrt (make-parameter one-of-the above)
Rather than mint new identifiers, one could also export the function via
multiple submodules, each of which has a different level of contracting. The
advantage is that the "safety level" 1) can be adjusted by the caller, 2)
without having to change the name of the identifier in the code. Again, this
could all be automated through a macro:
(begin
(define (real-sqrt x)
;; no contract)
(provide real-sqrt)
(module+ precheck
(provide (contract-out [real-sqrt precheck-contract ···])))
(module+ allchecks
(provide (contract-out [real-sqrt allcheck-contract ···])))
)
And so on.
--
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.
