logiccomp / lsl

4 stars 2 forks source link

Have `check-contract` errors show inputs when outputs fail contract? #17

Closed dbp closed 9 months ago

dbp commented 9 months ago

Say I have a function like:

(: my-prop (-> (List Integer) True))
(define (my-prop loi)
   (= (length loi) 1))

And I run (check-contract my-prop). If it finds a counter-example, the error just reports that the contract was violated because #f was received when True was expected.

e.g., an error like:

--------------------
module-level tests > Unnamed test
. FAILURE
name:       check-contract
location:   48-unsaved-editor:7:0
params:     '(#<procedure:.../lsl-lib/no-gui.rkt:409:38>)

my-prop: contract violation
  expected: True
  given: #f
  blaming: anonymous-module
--------------------
0 success(es) 1 failure(s) 0 error(s) 1 test(s) run

Like with verify-contract, we should see the inputs that were generated when we see the failure.

camoy commented 9 months ago

It looks like this now, with a piece of code that will trigger the error (in the same format as verify-contract):

my-prop: verification failure
  counterexample: (my-prop '())
  error:
    my-prop: contract violation
      expected: True
      given: #f
      blaming: anonymous-module (as server)