Re: [racket-dev] Announcing Soft Contract Verification tool
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 current build; it's adapted from Leif's commits at [1]. ;; --- Please keep the bug reports coming! > It looks like the built-in function expt isn't defined correctly: (module f racket (provide (contract-out [f (integer? . -> . integer?)])) (define (f n) (expt n n))) Contract violation: 'f' violates 'expt'. Wrong arity An example module that breaks it: (module user racket (require (submid ".." f)) (f 0)) (verification takes 0.035s) [1] https://github.com/LeifAndersen/racket/tree/no-conracts From e3a07fa756f47e0eb93be0811f245f1f814f028e Mon Sep 17 00:00:00 2001 From: ben Date: Sun, 18 Jan 2015 18:51:48 -0500 Subject: [PATCH] imported leif's no-contract changes --- racket/collects/racket/contract/private/base.rkt | 7 +- .../collects/racket/contract/private/provide.rkt | 80 +++--- 2 files changed, 43 insertions(+), 44 deletions(-) diff --git a/racket/collects/racket/contract/private/base.rkt b/racket/collects/racket/contract/private/base.rkt index c7bb61c..cf0ca33 100644 --- a/racket/collects/racket/contract/private/base.rkt +++ b/racket/collects/racket/contract/private/base.rkt @@ -35,13 +35,10 @@ (define-syntax (contract stx) (syntax-case stx () [(_ c v pos neg name loc) - (syntax/loc stx - (apply-contract c v pos neg name loc))] + (syntax/loc stx v)] [(_ c v pos neg) (with-syntax ([name (syntax-local-infer-name stx)]) - (syntax/loc stx -(apply-contract c v pos neg 'name -(build-source-location #f] + (syntax/loc stx v))] [(_ c v pos neg src) (raise-syntax-error 'contract (string-append diff --git a/racket/collects/racket/contract/private/provide.rkt b/racket/collects/racket/contract/private/provide.rkt index 5356a64..b020493 100644 --- a/racket/collects/racket/contract/private/provide.rkt +++ b/racket/collects/racket/contract/private/provide.rkt @@ -350,42 +350,44 @@ (raise-syntax-error #f "expected an identifier" stx #'new-id)) (unless (identifier? #'orig-id) (raise-syntax-error #f "expected an identifier" stx #'orig-id)) - (define-values (pos-blame-party-expr srcloc-expr) -(let loop ([kwd-args (syntax->list #'(kwd-args ...))] - [pos-blame-party-expr #'(quote-module-path)] - [srcloc-expr #f]) - (cond -[(null? kwd-args) (values pos-blame-party-expr - (or srcloc-expr (stx->srcloc-expr stx)))] -[else - (define kwd (car kwd-args)) - (cond - [(equal? (syntax-e kwd) '#:pos-source) -(when (null? (cdr kwd-args)) - (raise-syntax-error #f "expected a keyword argument to follow #:pos-source" - stx)) -(loop (cddr kwd-args) - (cadr kwd-args) - srcloc-expr)] - [(equal? (syntax-e kwd) '#:srcloc) -(when (null? (cdr kwd-args)) - (raise-syntax-error #f "expected a keyword argument to follow #:srcloc" - stx)) -(loop (cddr kwd-args) - pos-blame-party-expr - (cadr kwd-args))] - [else -(raise-syntax-error #f "expected either the keyword #:pos-source of #:srcloc" -stx -(car kwd-args))])]))) - (internal-function-to-be-figured-out #'ctrct - #'orig-id - #'orig-id - #'new-id - #'new-id - srcloc-expr - 'define-module-boundary-contract - pos-blame-party-expr))])])) + (define new-id orig-id) + ;; (define-values (pos-blame-party-expr srcloc-expr) + ;; (let loop ([kwd-args (syntax->list #'(kwd-args ...))] + ;; [pos-blame-party-expr #'(quote-module-path)] + ;; [srcloc-expr #f]) + ;; (cond + ;; [(null? kwd-args) (values pos-blame-party-expr + ;; (or srcloc-expr (stx->srcloc-expr stx)))] + ;; [else + ;;(define kwd (car kwd-args)) + ;;
Re: [racket-dev] Announcing Soft Contract Verification tool
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-check. Is there a similarly simple/standard way to disable contracts? Last I checked, I couldn't find one. So I think we each write our own my-define/contract and my-contract-out sort of macros? It's not difficult. But it's idiosyncratic. Also: tools. Why not e.g. #lang racket/no-check, and a racket/contract/no-check to require for use with #lang racket/base? Although I guess a tool like SCV is more in the business of disabling individual contracts; not so much whole-file granularity? _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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 like the web interface too. >> >> I was confused by this interaction though. Clicking verify on >> this: >> >> (module fact racket (define (factorial x) (if (zero? x) 1 (* x >> (factorial (sub1 x) (provide (contract-out [factorial (-> (>=/c >> 0) (>=/c 0))]))) >> >> gives me: >> >> 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) >> >> but the value 0.105 shouldn't violate the predicate real? I think. > > This is reporting that the fact module can break the contract on >= > when it uses >=/c; that's a bug in our modelling of >=/c, which we > currently have as: > > (define (>=/c n) > (lambda (m) > (>= m n))) > > But should be: > > (define (>=/c n) > (lambda (m) > (and (real? m) > (>= m n > > That said, if you change it to (and/c real? (>=/c 0)), it says there's > a counterexample of 2.0, but that's because we check contracts on > recursive calls (and should not). I misspoke on the issue of boundaries, which we had right, but there was another bug that's now fixed. We also fixed the >=/c implies real? bug. So to summarize, Asumu's program now verifies: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (-> (>=/c 0) (>=/c 0))]))) A slight variant that uses unsafe contracts will generate counterexamples causing fact to be blamed: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (-> (λ (x) (>= x 0)) (λ (x) (>= x 0)))]))) The counterexample is: (module user racket (require (submod ".." fact)) (begin (struct s₃ ()) (factorial (s₃ David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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?)])) > > (define (positive? x) > (and (integer? x) (<= 0 x))) > > (define (divides? a b) > (cond [(= 0 b) #t] > [(< b a) #f] > [else (divides? a (- b a))])) > > ) There was a bug causing this to loop which has been fixed. The server verifies this program now. Please keep the bug reports coming! David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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 x))) (define (divides? a b) (cond [(= 0 b) #t] [(< b a) #f] [else (divides? a (- b a))])) ) On Thu, Jan 15, 2015 at 3:14 PM, David Van Horn wrote: > 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 is coming in here. Can > > you explain more? > > On further inspection, the counterexample is wrong. (There are > counterexamples due to the model of >=/c, but the one that reported is > not an actual one.) This will be fixed shortly. > > David > > _ > Racket Developers list: > http://lists.racket-lang.org/dev > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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 is coming in here. Can > you explain more? On further inspection, the counterexample is wrong. (There are counterexamples due to the model of >=/c, but the one that reported is not an actual one.) This will be fixed shortly. David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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, 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 like the web interface too. >> >> I was confused by this interaction though. Clicking verify on >> this: >> >> (module fact racket (define (factorial x) (if (zero? x) 1 (* x >> (factorial (sub1 x) (provide (contract-out [factorial (-> (>=/c >> 0) (>=/c 0))]))) >> >> gives me: >> >> 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) >> >> but the value 0.105 shouldn't violate the predicate real? I think. > > This is reporting that the fact module can break the contract on >= > when it uses >=/c; that's a bug in our modelling of >=/c, which we > currently have as: > > (define (>=/c n) > (lambda (m) > (>= m n))) > > But should be: > > (define (>=/c n) > (lambda (m) > (and (real? m) > (>= m n > > That said, if you change it to (and/c real? (>=/c 0)), it says there's > a counterexample of 2.0, but that's because we check contracts on > recursive calls (and should not). > > Thanks! > > David > > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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 this interaction though. Clicking verify on > this: > > (module fact racket (define (factorial x) (if (zero? x) 1 (* x > (factorial (sub1 x) (provide (contract-out [factorial (-> (>=/c > 0) (>=/c 0))]))) > > gives me: > > 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) > > but the value 0.105 shouldn't violate the predicate real? I think. This is reporting that the fact module can break the contract on >= when it uses >=/c; that's a bug in our modelling of >=/c, which we currently have as: (define (>=/c n) (lambda (m) (>= m n))) But should be: (define (>=/c n) (lambda (m) (and (real? m) (>= m n That said, if you change it to (and/c real? (>=/c 0)), it says there's a counterexample of 2.0, but that's because we check contracts on recursive calls (and should not). Thanks! David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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) Hmm, actually I should've looked at this more carefully. Is this a case where the tool is telling me that the function is non-terminating on this input? Cheers, Asumu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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 >> 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: > > (module fact racket > (define (factorial x) > (if (zero? x) > 1 > (* x (factorial (sub1 x) > (provide (contract-out [factorial (-> (>=/c 0) (>=/c 0))]))) > > gives me: > > 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) > > but the value 0.105 shouldn't violate the predicate real? I think. > > Cheers, > Asumu > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (-> (>=/c 0) (>=/c 0))]))) gives me: 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) but the value 0.105 shouldn't violate the predicate real? I think. Cheers, Asumu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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: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 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 _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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: >>> >>> >>> 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 (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
Re: [racket-dev] Announcing Soft Contract Verification tool
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, 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
Re: [racket-dev] Announcing Soft Contract Verification tool
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 >>> 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
Re: [racket-dev] Announcing Soft Contract Verification tool
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 (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? _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
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. David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [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 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
