[racket-dev] Announcing Soft Contract Verification tool

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?

That said, I don't see how the bug in >=/c is coming in here. Can you
explain more?

Robby


On Thu, Jan 15, 2015 at 1:42 PM, David Van Horn <dvanhorn at cs.umd.edu> wrote:
> 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
>
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev