[racket-dev] Announcing Soft Contract Verification tool

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 <dvanhorn at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20150115/5fd16860/attachment.html>