[racket-dev] Announcing Soft Contract Verification tool

On 1/15/15 2:42 PM, David Van Horn 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).


I misspoke on the issue of boundaries, which we had right, but there
was another bug that's now fixed.  We also fixed the >=/c implies
real? bug.

So to summarize, Asumu's program now verifies:

  (module fact racket
    (define (factorial x)
      (if (zero? x)
          1
          (* x (factorial (sub1 x)))))

    (provide
      (contract-out
        [factorial (-> (>=/c 0) (>=/c 0))])))

A slight variant that uses unsafe contracts will generate
counterexamples causing fact to be blamed:

  (module fact racket
    (define (factorial x)
      (if (zero? x)
          1
          (* x (factorial (sub1 x)))))

    (provide
     (contract-out
      [factorial (-> (λ (x) (>= x 0))
                     (λ (x) (>= x 0)))])))

The counterexample is:

 (module user racket
   (require (submod ".." fact))
   (begin (struct s₃ ()) (factorial (s₃))))

David