[racket-dev] Announcing Soft Contract Verification tool

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.

David