[racket-dev] Announcing Soft Contract Verification tool

On 1/15/15 7:42 PM, Benjamin Greenman wrote:
> 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))]))
> 
> )


There was a bug causing this to loop which has been fixed.  The server
verifies this program now.

Please keep the bug reports coming!

David