Re: [racket-users] Apropos contracts: simple predicates and switching on and off

```Putting this new set-up through its paces I think I've found a few issues:

*1. Default argument goes missing from post-condition, leading to an
unexpected error ...*```
```
(define/contract (greater-than-square? x [y 0])
(->i ([x real?])
([y real?])
[result boolean?]
#:post (x y result)
(equal? result (< (sqr y) x)))

(> x (sqr y)))

(greater-than-square? 10)

sqr: contract violation
expected: number?
given: #<unsupplied-arg>

*2. contract-exercise seems to miss explicit #pre-conditions ...*

(contract-exercise sqrt2) finds no counter-examples (correct)
(contract-exercise sqrt3) finds bogus counter-examples (incorrect),
typically -inf.0 and -1

(define/contract (real-sqrt2 x)
(-> (>=/c 0) (>=/c 0))
(sqrt x))

(define/contract (real-sqrt3 x)
(->i ([x real?])
#:pre (x)
(>= x 0)
[result (>=/c 0)])
(sqrt x))

*3. post-conditions appear to be called twice ...*

Is there a double boundary crossing on post-conditions?

Output from instrumenting of (real-sqrt 100), Newton's method for
calculating the sqrt loaded with contracts (source code at end of e-mail)
...

> (real-sqrt 100 1e-14)

(10.0 0.0)
(10.0 0.0)
(10.000000000139897 2.7979396577393345e-11)
(10.000000000139897 2.7979396577393345e-11)
(10.000052895642693 1.0579156517920296e-05)
(10.000052895642693 1.0579156517920296e-05)
(10.032578510960604 0.0065263157858850285)
(10.032578510960604 0.0065263157858850285)
(10.840434673026925 0.17515023900164373)
(10.840434673026925 0.17515023900164373)
(15.025530119986813 1.257665553866309)
(15.025530119986813 1.257665553866309)
(26.24009900990099 5.88542796049407)
(26.24009900990099 5.88542796049407)
(50.5 24.5025)
10.0

Note: The reverse order is because of the nature of the recursion — to be
useful in catching errors in runaway computations the check should be moved
to the pre-condition.

* * *

Finally, some timings.

Stripping out the contracts to get a fast implementation for comparison:

(define (real-sqrt-fast x [eps 1e-14])
(define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x))))

(define (S estimate)
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))

(if (zero? x)
0
(S x)))

More moderate choice of contracts:

(define/contract (real-sqrt-moderate x [eps 1e-14])
(->* ((>=/c 0)) ((>/c 0)) (>=/c 0))
(define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x))))

(define/tight (S estimate)
(-> (and (>/c 0) (<=/c (max 1 x))) (>/c 0))
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))

(if (zero? x)
0
(S x)))

The fully contract-loaded code is at the end of this email (just comment
out the displayln).

Timing code:

(time
(for/last ([i (in-range 1000)])
(real-sqrt 1000 1e-14)))

(time
(for/last ([i (in-range 1000)])
(real-sqrt-moderate 1000)))

(time
(for/last ([i (in-range 1000)])
(real-sqrt-fast 1000)))

*All the contracts*
cpu time: 840 real time: 1048 gc time: 288
31.622776601683793

*Moderate (but still some "tight") use of contracts *
cpu time: 404 real time: 443 gc time: 163
31.622776601683793

*No contracts*
cpu time: 3 real time: 3 gc time: 0
31.622776601683793

So a 280x speed-up / slow-down for heavy-duty use of "tight" contracts. ;-)
Only a factor of 2x difference between the contract variations.

Dan

Contracts for real-sqrt

#lang racket

(define-syntax-rule (define/tight (fn args ...)
ctc
body ...)
(begin
(define (fn args ...) (fn/impl args ...))
(with-contract fn
([fn/impl ctc])
#:freevar fn ctc
(define (fn/impl args ...)
body ...))))

(define-syntax-rule (implies a b)
(or (not a) b))

(define (sqrt-error x estimate)
(-> (>/c 0) (>/c 0) (>=/c 0))
(abs (- 1 (/ (sqr estimate) x))))

(define/contract (real-sqrt x eps)
(->i ([x (>=/c 0)]
[eps (>/c 0)])
[result (>=/c 0)]
#:post (x result)
(implies (= x 0) (= result 0))
#:post (x eps result)
(implies (> x 0) (< (sqrt-error x result) eps)))

(define/tight (S estimate)
(->i ([estimate (and (>/c 0) (<=/c (max 1 x)))])
[result (>/c 0)]
#:post/name (estimate result)
"Unless it is practically zero, the error should decrease with
every iteration"
(let ([dr (sqrt-error x result)])
(displayln (list estimate (sqrt-error x estimate)))
(or (< dr eps)
(< dr (sqrt-error x estimate)))))

(if (< (sqrt-error x estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))

(if (zero? x)
0
(S (* 0.5 (+ 1 x)))))

(define (real-sqrt-fast x [eps 1e-14])
(define (error estimate)
(abs (- 1 (/ (sqr estimate) x))))

(define (S estimate)
(if (< (error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))

(if (zero? x)
0
(S x)))

--
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