[racket-dev] Announcing Soft Contract Verification tool

Argh, I wanted the other way (negative). I always get the directions confused. Sorry. 



On Jan 15, 2015, at 11:26 AM, David Van Horn <dvanhorn at 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 <dvanhorn at 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
>