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
happening?
(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:
http://lists.racket-lang.org/dev
