[racket-dev] Announcing Soft Contract Verification tool

FWIW, (</c 0) already implies real?.

Robby

On Thu, Jan 15, 2015 at 10:30 AM, David Van Horn <dvanhorn at 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 <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
>>>
>
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev