[racket-dev] Announcing Soft Contract Verification tool

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 <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
>>