I tried writing a small program, but got stuck pretty early on. When I try
verifying the "divides?" function below, the tool times out. What's

(module div racket
  (provide (contract-out [divides? (-> positive? positive? boolean?)]))

  (define (positive? x)
    (and (integer? x) (<= 0 x)))

  (define (divides? a b)
    (cond [(= 0 b) #t]
          [(< b a) #f]
          [else (divides? a (- b a))]))


On Thu, Jan 15, 2015 at 3:14 PM, David Van Horn <dvanh...@cs.umd.edu> wrote:

> On 1/15/15, 2:48 PM, Robby Findler wrote:
> > Can you randomly make up programs from your grammar, get example
> > errors from the tool, and then run those programs to see if you
> > find bugs in the analysis like that one?
> Yes, we're planning to do this.
> > That said, I don't see how the bug in >=/c is coming in here. Can
> > you explain more?
> On further inspection, the counterexample is wrong.  (There are
> counterexamples due to the model of >=/c, but the one that reported is
> not an actual one.)  This will be fixed shortly.
> David
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev
  Racket Developers list:

Reply via email to