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