Changeset 31105 in project


Ignore:
Timestamp:
07/08/14 13:55:49 (6 years ago)
Author:
juergen
Message:

dbc version 1.0.3 docu improved

File:
1 edited

Legend:

Unmodified
Added
Removed
  • wiki/eggref/4/dbc

    r28520 r31105  
    303303<macro>(command-contract ((old new query) ....) (pat pre post) ....)</macro>
    304304
    305 hygienic, keys ()
    306 
    307 <enscript highlight=scheme>
    308 
    309 (command-contract ((old new query) ....) (pat pre post) ....)
    310   (lambda-list? pat)
    311   (contract? result)
    312 
     305<enscript highlight=scheme>
     306hygienic, keys ()
     307requires (lambda-list? pat)
     308ensures  (contract? result)
    313309</enscript>
    314310
     
    317313<macro>(contract (result ....) (pat pre post) ....)</macro>
    318314
    319 hygienic, keys ()
    320 
    321 <enscript highlight=scheme>
    322 
    323 (contract (result ....) (pat pre post) ....)
    324   (lambda-list? pat)
    325   (contract? result)
    326 
     315<enscript highlight=scheme>
     316hygienic, keys ()
     317requires (lambda-list? pat)
     318ensures  (contract? result)
    327319</enscript>
    328320
     
    331323<procedure>(contract-arguments cnd)</procedure>
    332324
    333 function (result)
    334 
    335 <enscript highlight=scheme>
    336 
    337 (contract-arguments cnd)
    338   (contract-condition? cnd)
    339   (list? result)
    340 
     325<enscript highlight=scheme>
     326function (result)
     327requires (contract-condition? cnd)
     328ensures  (list? result)
    341329</enscript>
    342330
    343331==== contract-check-level
    344332
    345 <parameter>(or (contract-check-level) (contract-check-level x))</parameter>
    346 
    347 (or (result) ((old new (lambda (x) (contract-check-level)))))
    348 
    349 <enscript highlight=scheme>
    350 
    351 (contract-check-level)
    352   (and (integer? result)
    353        (<= 0 result 2)
    354        "0: no checks, 1: preconditions checked, 2: pre- and postconditions checked")
    355 
    356 (contract-check-level x)
    357   (and (integer? x) (<= 0 x 2))
    358   (= new x)
    359 
     333<parameter>(contract-check-level x ..)</parameter>
     334
     335<enscript highlight=scheme>
     336requires (and (integer? x)
     337              (<= 0 x 2)
     338              "0: no checks"
     339              "1: preconditions checked"
     340              "2: pre- and postconditions checked")
    360341</enscript>
    361342
     
    364345<procedure>(contract-condition-handler exn)</procedure>
    365346
    366 function (result)
    367 
    368 <enscript highlight=scheme>
    369 
    370 (contract-condition-handler exn)
    371   (condition? exn)
    372   "result of handled exeption"
    373 
     347<enscript highlight=scheme>
     348function (result)
     349requires (condition? exn)
     350ensures  result of handled exeption
    374351</enscript>
    375352
     
    378355<procedure>(contract-condition? xpr)</procedure>
    379356
    380 function (result)
    381 
    382 <enscript highlight=scheme>
    383 
    384 (contract-condition? xpr)
    385   #t
    386   (boolean? result)
    387 
     357<enscript highlight=scheme>
     358function (result)
     359requires #t
     360ensures  (boolean? result)
    388361</enscript>
    389362
     
    392365<procedure>(contract-location cnd)</procedure>
    393366
    394 function (result)
    395 
    396 <enscript highlight=scheme>
    397 
    398 (contract-location cnd)
    399   (contract-condition? cnd)
    400   (symbol? result)
    401 
     367<enscript highlight=scheme>
     368function (result)
     369requires (contract-condition? cnd)
     370ensures  (symbol? result)
    402371</enscript>
    403372
     
    406375<procedure>(contract-text cnd)</procedure>
    407376
    408 function (result)
    409 
    410 <enscript highlight=scheme>
    411 
    412 (contract-text cnd)
    413   (contract-condition? cnd)
    414   (string? result)
    415 
     377<enscript highlight=scheme>
     378function (result)
     379requires (contract-condition? cnd)
     380ensures  (string? result)
    416381</enscript>
    417382
     
    420385<procedure>(contract? xpr)</procedure>
    421386
    422 function (result)
    423 
    424 <enscript highlight=scheme>
    425 
    426 (contract? xpr)
    427   #t
    428   (boolean? result)
    429 
     387<enscript highlight=scheme>
     388function (result)
     389requires #t
     390ensures  (boolean? result)
    430391</enscript>
    431392
     
    434395<macro>(define-macro-with-contract name contr (transformer-type proc))</macro>
    435396
    436 hygienic, keys ()
    437 
    438 <enscript highlight=scheme>
    439 
    440 (define-macro-with-contract name contr (transformer-type proc))
    441   (contract? contr)
    442   (begin
    443     (push-contract! (car (contr (quote name))))
    444     (define-syntax name
    445       (transformer-type ((cdr (contr (quote name))) proc))))
    446 
     397<enscript highlight=scheme>
     398hygienic, keys ()
     399requires (contract? contr)
     400ensures  (begin (push-contract! (car (contr (quote name)))) (define-syntax name (transformer-type ((cdr (contr (quote name))) proc))))
    447401</enscript>
    448402
     
    451405<macro>(define-with-contract name contr proc)</macro>
    452406
    453 hygienic, keys ()
    454 
    455 <enscript highlight=scheme>
    456 
    457 (define-with-contract name contr proc)
    458   (contract? contr)
    459   (begin
    460     (push-contract! (car (contr (quote name))))
    461     (define name ((cdr (contr (quote name))) proc)))
    462 
     407<enscript highlight=scheme>
     408hygienic, keys ()
     409requires (contract? contr)
     410ensures  (begin (push-contract! (car (contr (quote name)))) (define name ((cdr (contr (quote name))) proc)))
    463411</enscript>
    464412
     
    467415<macro>(exit-dbc-with name)</macro>
    468416
    469 hygienic, keys ()
    470 
    471 <enscript highlight=scheme>
    472 
    473 (exit-dbc-with name)
    474   (symbol? name)
    475   "saves *contracts* in dispatcher name"
    476 
     417<enscript highlight=scheme>
     418hygienic, keys ()
     419requires (symbol? name)
     420ensures  saves *contracts* in dispatcher name
    477421</enscript>
    478422
     
    481425<macro>(init-dbc)</macro>
    482426
    483 not hygienic, exports *contracts*, keys ()
    484 
    485 <enscript highlight=scheme>
    486 
    487 (init-dbc)
    488   #t
    489   "initializes exception handler"
    490 
     427<enscript highlight=scheme>
     428unhygienic, exports *contracts* keys ()
     429requires #t
     430ensures  initializes exception handler
    491431</enscript>
    492432
     
    495435<procedure>(lambda-list? xpr)</procedure>
    496436
    497 function (result)
    498 
    499 <enscript highlight=scheme>
    500 
    501 (lambda-list? xpr)
    502   #t
    503   (boolean? result)
    504 
     437<enscript highlight=scheme>
     438function (result)
     439requires #t
     440ensures  (boolean? result)
    505441</enscript>
    506442
     
    509445<macro>(macro-contract hyg ... (key ...) (pat fender matcher) ....)</macro>
    510446
    511 hygienic, keys ()
    512 
    513 <enscript highlight=scheme>
    514 
    515 (macro-contract hyg ... (key ...) (pat fender matcher) ....)
    516   (and (nested-lambda-list? pat) (procedure? matcher))
    517   (contract? result)
    518 
     447<enscript highlight=scheme>
     448hygienic, keys ()
     449requires (and (nested-lambda-list? pat) (procedure? matcher))
     450ensures  (contract? result)
    519451</enscript>
    520452
     
    523455<procedure>(make-contract-condition location text . arguments)</procedure>
    524456
    525 function (result)
    526 
    527 <enscript highlight=scheme>
    528 
    529 (make-contract-condition location text . arguments)
    530   (and (symbol? location) (string? text))
    531   (condition? result)
    532 
     457<enscript highlight=scheme>
     458function (result)
     459requires (and (symbol? location) (string? text))
     460ensures  (condition? result)
    533461</enscript>
    534462
     
    537465<procedure>(make-dispatcher alist)</procedure>
    538466
    539 function (result)
    540 
    541 <enscript highlight=scheme>
    542 
    543 (make-dispatcher alist)
    544   ((list-of? list?) alist)
    545   (procedure? result)
    546 
     467<enscript highlight=scheme>
     468function (result)
     469requires ((list-of? list?) alist)
     470ensures  (procedure? result)
    547471</enscript>
    548472
     
    551475<macro>(matches? pat . fenders)</macro>
    552476
    553 hygienic, keys ()
    554 
    555 <enscript highlight=scheme>
    556 
    557 (matches? pat . fenders)
    558   (nested-lambda-list? pat)
    559   "procedure returning #t if its argument matches pat with fenders"
    560 
     477<enscript highlight=scheme>
     478hygienic, keys ()
     479requires (nested-lambda-list? pat)
     480ensures  procedure returning #t if its argument matches pat with fenders
    561481</enscript>
    562482
     
    565485<procedure>(nested-lambda-list? xpr)</procedure>
    566486
    567 function (result)
    568 
    569 <enscript highlight=scheme>
    570 
    571 (nested-lambda-list? xpr)
    572   #t
    573   (boolean? result)
    574 
     487<enscript highlight=scheme>
     488function (result)
     489requires #t
     490ensures  (boolean? result)
    575491</enscript>
    576492
     
    579495<macro>(push-contract! contract-docu)</macro>
    580496
    581 hygienic, keys ()
    582 
    583 <enscript highlight=scheme>
    584 
    585 (push-contract! contract-docu)
    586   "documentation of a contract"
    587   (matches? (set! *contracts* (cons contract-docu *contracts*)))
    588 
     497<enscript highlight=scheme>
     498hygienic, keys ()
     499requires documentation of a contract
     500ensures  (matches? (set! *contracts* (cons contract-docu *contracts*)))
    589501</enscript>
    590502
     
    593505<procedure>(string-repeat str n)</procedure>
    594506
    595 function (result)
    596 
    597 <enscript highlight=scheme>
    598 
    599 (string-repeat str n)
    600   (and (string? str) (not (negative? n)))
    601   (string? result)
    602 
     507<enscript highlight=scheme>
     508function (result)
     509requires (and (string? str) (not (negative? n)))
     510ensures  (string? result)
    603511</enscript>
    604512
     
    609517== Last update
    610518
    611 Feb 09, 2013
     519Jul 08, 2014
    612520
    613521== License
     
    625533
    626534== Version History
     535; 1.0.3 : document-contracts changed
    627536; 1.0.2 : document-contracts changed again, run-tests used
    628537; 1.0.1 : document-contracts changed
Note: See TracChangeset for help on using the changeset viewer.