[racket-dev] Announcing Soft Contract Verification tool

I think this is saying that the result is going to be negative. (But
it won't, since it doesn't terminate.)

Robby


On Thu, Jan 15, 2015 at 1:13 PM, Asumu Takikawa <asumu at ccs.neu.edu> 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.
>
> Cheers,
> Asumu
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev