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? On Jan 14, 2015, at 7:11 PM, David Van Horn <dvanh...@cs.umd.edu> wrote: > Racketeers, > > 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: > > http://scv.umiacs.umd.edu > > 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 > programs. > > 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: > http://lists.racket-lang.org/dev _________________________ Racket Developers list: http://lists.racket-lang.org/dev