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 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Reply via email to