On 1/15/15, 11:27 AM, Matthias Felleisen wrote: > > Argh, I wanted the other way (negative). I always get the > directions confused. Sorry.
Right -- using (and/c real? (</c 0)) will also make this verify. Thanks for trying it out! David > > > On Jan 15, 2015, at 11:26 AM, David Van Horn <dvanh...@cs.umd.edu> > wrote: > >> On 1/15/15, 11:17 AM, Matthias Felleisen wrote: >>> >>> >>> On Jan 15, 2015, at 11:13 AM, David Van Horn >>> <dvanh...@cs.umd.edu> wrote: >>> >>>> On 1/15/15, 11:04 AM, Matthias Felleisen wrote: >>>>> >>>>> Well that got me all excited. So I tried to get the sample >>>>> module to pass the verification step -- until I realized >>>>> how restricted the grammar is! >>>>> >>>>> (module f racket (provide (contract-out [f (real? . -> . >>>>> integer?)])) (define (f n) (/ 1 (- 100 n)))) >>>>> >>>>> I would love to be able to use at least (and/c real? (>/c >>>>> 0)) for the domain so I can get the example done. >>>>> >>>>> Or am I overlooking a way to make this work here? >>>> >>>> The >/c contract is there, but missing from the grammar >>>> (we'll fix that). >>>> >>>> But (>/c 0) will not make this program verify. You want >>>> this contract: >>>> >>>> ((and/c real? (lambda (x) (not (= x 100)))) . -> . real?) >>>> >>>> Using this contract, the program verifies. >>> >>> >>> My contract is stronger than yours. So why will it not go >>> through? >>> >>> >> >> 100 is (>/c 0) but (f 100) divides by zero. >> >> David >> _________________________ Racket Developers list: http://lists.racket-lang.org/dev
