Re: [racket-dev] Announcing Soft Contract Verification tool

2015-01-16 Thread David Van Horn 
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

2015-01-16 Thread David Van Horn 
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] [racket] Implementing contracts for async channels

2015-01-16 Thread Alexis King 
Ah, that makes sense, fixed.

 On Jan 16, 2015, at 05:37, Robby Findler ro...@eecs.northwestern.edu wrote:
 
 One comment. The contract combinators are curried so that you can do
 work on the partial applications. So don't write this:
 
 (define ho-val-first-projection
 impersonate/chaperone-async-channel) ctc) blame) val)
 
 instead try to do some work earlier, when you first can. (The most
 important thing is to minimize the work done after you get the 'val'
 argument.)
 
 Robby


_
  Racket Developers list:
  http://lists.racket-lang.org/dev