[racket-dev] Announcing Soft Contract Verification tool

On 1/15/15, 2:13 PM, Asumu Takikawa wrote:
> On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
>> If you have questions, comments, bugs, or any other feedback, let
>> us know, or just file bug reports on the GitHub source code.
> 
> Nice tool! I like the web interface too.
> 
> I was confused by this interaction though. Clicking verify on
> this:
> 
> (module fact racket (define (factorial x) (if (zero? x) 1 (* x
> (factorial (sub1 x))))) (provide (contract-out [factorial (-> (>=/c
> 0) (>=/c 0))])))
> 
> gives me:
> 
> Contract violation: 'fact' violates '>='. Value 0.105 violates
> predicate real? An example module that breaks it: (module user
> racket (require (submod ".." fact)) (factorial 0.105)) 
> (Verification takes 0.05s)
> 
> but the value 0.105 shouldn't violate the predicate real? I think.

This is reporting that the fact module can break the contract on >=
when it uses >=/c; that's a bug in our modelling of >=/c, which we
currently have as:

(define (>=/c n)
  (lambda (m)
    (>= m n)))

But should be:

(define (>=/c n)
  (lambda (m)
    (and (real? m)
         (>= m n))))

That said, if you change it to (and/c real? (>=/c 0)), it says there's
a counterexample of 2.0, but that's because we check contracts on
recursive calls (and should not).

Thanks!

David