FWIW, (</c 0) already implies real?. Robby
On Thu, Jan 15, 2015 at 10:30 AM, David Van Horn <dvanh...@cs.umd.edu> wrote: > 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 _________________________ Racket Developers list: http://lists.racket-lang.org/dev
