[racket-dev] Announcing Soft Contract Verification tool

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