While trying to express in the contract system Daniel Prager's check that a
possibly-buggy square root function actually returns the square root of its
argument (and in particular the nice error messages, I ran into a few
things that weren't quite as I expected.
My first attempt, using flat-contract-with-explanation, looks like this:
(define/contract (squares-to/within/c x error)
(-> (>=/c 0) (>=/c 0) flat-contract?)
(flat-contract-with-explanation
(λ (rslt)
(cond
[(not (real? rslt))
(λ (blame)
(raise-blame-error
blame rslt
'(expected: "real?" given: "~e")
rslt))]
[(<= (abs (- x (* rslt rslt)))
error)
#t]
[else
(λ (blame)
(raise-blame-error
blame rslt
'(expected:
"a number that squares to ~e ± ~e"
given: "~e"
"\n " given " squared: ~e")
x error rslt (* rslt rslt)))]))))
(define/contract (buggy-sqrt x)
(->i ([x (>=/c 0)])
[rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>/c 0)
(squares-to/within/c x 0.0000001)))])
1)
(Aside: I noticed that despite this thread, flat-contract-with-explanation
still does not accept a #:name argument, or at least not in 6.9.)
Given the above, (buggy-sqrt 4) produces this fairly unhelpful error
message, including none of the nice reporting:
buggy-sqrt: broke its own contract
promised: (and/c (and/c real? positive?) anonymous-flat-contract)
produced: 1
in: the rslt result of
(->i
((x (and/c real? (not/c negative?))))
(rslt
(x)
(if (= 0 x)
(=/c 0)
(and/c
(>/c 0)
(squares-to/within/c x 1e-07)))))
contract from: (function buggy-sqrt)
blaming: (function buggy-sqrt)
(assuming the contract is correct)
at: unsaved-editor:26.18
I then tried dropping down to make-flat-contract like this:
(define/contract (squares-to/within/c-v2 x error)
(-> (>=/c 0) (>=/c 0) flat-contract?)
(make-flat-contract
#:name `(squares-to/within/c-v2 ,x ,error)
#:first-order (λ (rslt)
(and (real? rslt)
(<= (abs (- x (* rslt rslt)))
error)))
#:late-neg-projection
(λ (blame)
(λ (rslt neg-party)
(cond
[(not (real? rslt))
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected: "real?" given: "~e")
rslt)]
[(<= (abs (- x (* rslt rslt)))
error)
rslt]
[else
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected:
"a number that squares to ~e ± ~e"
given: "~e"
"\n " given " squared: ~e")
x error rslt (* rslt rslt))])))))
(define/contract (buggy-sqrt-v2 x)
(->i ([x (>=/c 0)])
[rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>/c 0)
(squares-to/within/c-v2 x 0.0000001)))])
1)
but (buggy-sqrt-v2 4) gives this error:
buggy-sqrt-v2: broke its own contract
promised: (and/c (and/c real? positive?) (squares-to/within/c-v2 4 1e-07))
produced: 1
in: the rslt result of
(->i
((x (and/c real? (not/c negative?))))
(rslt
(x)
(if (= 0 x)
(=/c 0)
(and/c
(>/c 0)
(squares-to/within/c-v2 x 1e-07)))))
contract from: (function buggy-sqrt-v2)
blaming: (function buggy-sqrt-v2)
(assuming the contract is correct)
at: unsaved-editor:67.18
which is improved only in that it includes a name: it still doesn't use the
nice error message I programed in, and it doesn't even tell me which case
of the and/c failed (though that is fairly obvious in this case).
Just for completeness, I also tried a struct, like so:
(struct squares-to/within-contract (x error)
#:property prop:custom-write contract-custom-write-property-proc
#:property prop:flat-contract
(build-flat-contract-property
#:name
(match-lambda
[(squares-to/within-contract x error)
`(squares-to/within/c-v3 ,x ,error)])
#:first-order
(match-lambda
[(squares-to/within-contract x error)
(λ (rslt)
(and (real? rslt)
(<= (abs (- x (* rslt rslt)))
error)))])
#:late-neg-projection
(match-lambda
[(squares-to/within-contract x error)
(λ (blame)
(λ (rslt neg-party)
(cond
[(not (real? rslt))
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected: "real?" given: "~e")
rslt)]
[(<= (abs (- x (* rslt rslt)))
error)
rslt]
[else
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected:
"a number that squares to ~e ± ~e"
given: "~e"
"\n " given " squared: ~e")
x error rslt (* rslt rslt))])))])))
(define/contract (squares-to/within/c-v3 x error)
(-> (>=/c 0) (>=/c 0) flat-contract?)
(squares-to/within-contract x error))
(define/contract (buggy-sqrt-v3 x)
(->i ([x (>=/c 0)])
[rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>/c 0)
(squares-to/within/c-v3 x 0.0000001)))])
1)
but (buggy-sqrt-v3 4) was like (buggy-sqrt-v2 4) except for the version
number.
I would also note that using the contract in e.g.
(define/contract buggy
(and/c number? (squares-to/within/c-v3 4 0.0000001))
1)
gives the nice error I wanted:
../../Applications/Racket v6.9/collects/racket/private/kw.rkt:1170:47:
buggy: broke its own contract
promised: a number that squares to 4 ± 1e-07
produced: 1
produced squared: 1
in: an and/c case of
(and/c
number?
(squares-to/within/c-v3 4 1e-07))
contract from: (definition buggy)
blaming: (definition buggy)
(assuming the contract is correct)
at: unsaved-editor:131.17
The error message just seems to be lost with some subset of combinators,
evidently including ->i.
-Philip
---------- Forwarded message ----------
From: Daniel Prager <daniel.a.pra...@gmail.com>
Date: Tue, May 2, 2017 at 5:01 PM
Subject: [racket-users] Apropos contracts: simple predicates and switching
on and off
To: Racket Users <racket-users@googlegroups.com>
#lang racket
(define pre-conditions-on #t)
(define post-conditions-on #t)
(define (implies a b)
(or (not a) b))
(define-syntax-rule (pre [test? msg] ...)
(unless (not pre-conditions-on)
(unless test?
(error (~a "Pre-condition violation: " msg))) ...))
(define-syntax-rule (post [test? msg] ...)
(unless (not post-conditions-on)
(unless test?
(error (~a "Post-condition violation: " msg))) ...))
(define (real-sqrt x)
(pre [(real? x) "real argument expected"]
[(>= x 0) "non-negative argument expected"])
(define result (sqrt x))
; Change the implementation to 1, 0, (- x) to trigger various
post-condition errors
(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)"])
result)
(real-sqrt 0)
(real-sqrt 9)
(real-sqrt -9) ; Pre-condition error
--
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.
