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
(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?
On Jan 14, 2015, at 7:11 PM, David Van Horn <dvanh...@cs.umd.edu> wrote:
> Over the last year, we've been working on a tool for automatically
> verifying that programs live up to their contracts. We're happy to
> announce that it's now available for people to try out here:
> You type in some modules in the editor, and click either Run or
> Verify. The Verify button uses our tool to determine if the modules
> always live up to their contract, and if they don't, it automatically
> generates a counterexample, showing how to break the module. There are
> a number of examples that you can play with, accessed via a menu on
> the site.
> Right now, the tool supports a fixed subset of Racket, but we're
> working on making it handle much more by analyzing fully-expanded
> There's explanations on the site to go along with each example
> program, and there's an "About" page with more info, and links to our
> papers about the work, at http://scv.umiacs.umd.edu/about
> We plan to release a command-line tool and a DrRacket plugin in the
> future, once we can handle more of Racket.
> If you have questions, comments, bugs, or any other feedback, let us
> know, or just file bug reports on the GitHub source code.
> Phil, David, Sam
> Racket Developers list:
Racket Developers list: