On Sun, Jan 18, 2015 at 9:44 AM, Greg Hendershott wrote:
> Is there a similarly simple/standard way to disable contracts?
I'd love a #lang like that. Never mind Tony Hoare's metaphor about sailing.
For now, I'm attaching a small patch that'll disable contracts (as far as I
can tell) on the curr
This looks really exciting!
Imagining using this reminds me of something.
Typed Racket has a simple/standard way to disable type-checking (while
retaining the type declarations for documentation value as well as
potential re-enabling): #lang typed/racket/no-check and #lang
typed/racket/base/no-ch
On 1/15/15 2:42 PM, David Van Horn wrote:
> On 1/15/15, 2:13 PM, Asumu Takikawa wrote:
>> On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
>>> If you have questions, comments, bugs, or any other feedback, let
>>> us know, or just file bug reports on the GitHub source code.
>>
>> Nice tool! I lik
On 1/15/15 7:42 PM, Benjamin Greenman wrote:
> I tried writing a small program, but got stuck pretty early on. When I
> try verifying the "divides?" function below, the tool times out. What's
> happening?
>
> (module div racket
> (provide (contract-out [divides? (-> positive? positive? boolean?)
I tried writing a small program, but got stuck pretty early on. When I try
verifying the "divides?" function below, the tool times out. What's
happening?
(module div racket
(provide (contract-out [divides? (-> positive? positive? boolean?)]))
(define (positive? x)
(and (integer? x) (<= 0
On 1/15/15, 2:48 PM, Robby Findler wrote:
> Can you randomly make up programs from your grammar, get example
> errors from the tool, and then run those programs to see if you
> find bugs in the analysis like that one?
Yes, we're planning to do this.
> That said, I don't see how the bug in >=/c i
Can you randomly make up programs from your grammar, get example
errors from the tool, and then run those programs to see if you find
bugs in the analysis like that one?
That said, I don't see how the bug in >=/c is coming in here. Can you
explain more?
Robby
On Thu, Jan 15, 2015 at 1:42 PM, Da
On 1/15/15, 2:13 PM, Asumu Takikawa wrote:
> On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
>> If you have questions, comments, bugs, or any other feedback, let
>> us know, or just file bug reports on the GitHub source code.
>
> Nice tool! I like the web interface too.
>
> I was confused by
On 2015-01-15 14:13:02 -0500, Asumu Takikawa wrote:
> Contract violation: 'fact' violates '>='.
> Value
> 0.105
> violates predicate
> real?
> An example module that breaks it:
> (module user racket (require (submod ".." fact)) (factorial 0.105))
> (Verification takes 0.05s)
I think this is saying that the result is going to be negative. (But
it won't, since it doesn't terminate.)
Robby
On Thu, Jan 15, 2015 at 1:13 PM, Asumu Takikawa wrote:
> On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
>> If you have questions, comments, bugs, or any other feedback, let us
On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
> If you have questions, comments, bugs, or any other feedback, let us
> know, or just file bug reports on the GitHub source code.
Nice tool! I like the web interface too.
I was confused by this interaction though. Clicking verify on this:
(m
FWIW, ( 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? (
> Thanks for trying it out!
>
> David
>
>>
>>
>> On Jan 15, 2015, at 11:26 AM, David Van Horn
>> 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? (
>
> On Jan 15, 2015, at 11:26 AM, David Van Horn
> wrote:
>
>> On 1/15/15, 11:17 AM, Matthias Felleisen wrote:
>>>
>>>
>>
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 wrote:
> On 1/15/15, 11:17 AM, Matthias Felleisen wrote:
>>
>>
>> On Jan 15, 2015, at 11:13 AM, David Van Horn
>> wrote:
>>
>>> On 1/15/15, 11:04 AM, Matthi
On 1/15/15, 11:17 AM, Matthias Felleisen wrote:
>
>
> On Jan 15, 2015, at 11:13 AM, David Van Horn
> 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
>
On Jan 15, 2015, at 11:13 AM, David Van Horn 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
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
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 lea
18 matches
Mail list logo
