[racket-dev] Announcing Soft Contract Verification tool

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