Buggy binary search example

binary-search-ce.rkt

(module lib racket
  (provide
   (contract-out
    ;; old model didn't have integer division
    [quotient (->i ([n (and/c integer? (>=/c 0))])
                   (res (n) (->i ([d (and/c integer? (>/c 0))])
                                 (res (d) (and/c integer?
                                                 (>=/c 0)
                                                 (λ (r) (<= (* r d) n)))))))]
    [length ((listof any/c) . -> . (and/c integer? (>=/c 0)))]
    [vect-ref (->i ([vect (listof integer?)])
                   (res (vect)
                        (-> (λ (index) (and (integer? index)
                                            (<= 0 index)
                                            (< index (length vect))))
                            integer?)))]))
  ;; Length needs to be concrete to relate a list's shape with its length
  (define (length xs) (if (null? xs) 0 (+ 1 (length (cdr xs))))))

(module binary-search racket
  (provide
   (contract-out
    [binary-search (integer?
                    (listof integer?)
                    . -> .
                    (or/c not integer?))]))

  (require (submod ".." lib))
  
  (define (binary-search v vec)
    (loop v vec 0 (length vec)))

  (define (loop v vec lo hi)
    (let ([mid ((quotient (+ lo hi)) 2)])
      (cond [(< v ((vect-ref vec) mid))
             (let ([hi* (- mid 1)])
               (if (<= lo hi*)
                   (loop v vec lo hi*)
                   #f))]
            [(< ((vect-ref vec) mid) v)
             (let ([lo* (+ mid 1)])
               (if (<= lo* hi)
                   (loop v vec lo* hi)
                   #f))]
            [else mid]))))