~nytpu/dbc-scheme

586b717ab97dfe406787c8657289cf40536e601d — nytpu 1 year, 9 months ago 4500b8d
update documentation
2 files changed, 20 insertions(+), 19 deletions(-)

M contracts.scm
M contracts.sld
M contracts.scm => contracts.scm +13 -18
@@ 19,13 19,6 @@
                         addl-irritants))))
    l1 l2))

;; Transform a series of expressions into a list of \scheme{quote}d
;; expressions.
(define-syntax quotify
  (syntax-rules ()
    ((_ q ...)
     (list (quote q) ...))))

;; \scheme{verify-contracts} will verify that a series of expressions returns
;; true, otherwise raising an exception with the quoted representation of the
;; expression that failed.


@@ 38,8 31,7 @@
;;     them return true.
;;   }
;;   \item{
;;     Given a series of thunk expressions, verify that all of them return
;;     true.
;;     Given a series of expressions, verify that all of them return true.
;;   }
;; ]
(define-syntax verify-contracts


@@ 50,28 42,28 @@
     (let ((return r))
       (if (execute-contracts (list (delay (c1 return))
                                    (delay (c2 return)) ...)
                              (quotify c1 c2 ...)
                              (list (quote c1) (quote c2) ...)
                              "postcondition assertion violation"
                              return)
           return
           #f)))
    ((_ c1 c2 ...)
     (execute-contracts (list (delay c1) (delay c2) ...)
                        (quotify c1 c2 ...)
                        (list (quote c1) (quote c2) ...)
                        "precondition assertion violation"))))

;;> Define a lambda expression as with \scheme{lambda}, however add
;;> precondition and/or postcondition contracts.
;;>
;;> Given a \scheme{(pre contracts ...)}, where \var{contracts ...} is zero
;;> or more thunk expressions, evaluate each thunk sequentially in the same
;;> scope as the function body.  If a thunk returns \scheme{#f}, then raise
;;> or more expressions, evaluate each thunk sequentially in the same scope
;;> as the function body.  If an expression returns \scheme{#f}, then raise
;;> an exception noting a precondition violation with the irritants being the
;;> (\scheme{quote}d) thunk that failed.
;;> (\scheme{quote}d) expression that failed.
;;>
;;> Given a \scheme{(post contracts ...)}, where \var{contracts ...} is zero
;;> or more predicate functions taking a single argument, evaluate each
;;> expression sequentially given the return value of the function; in the
;;> contract sequentially given the return value of the function; in the
;;> same scope as the function body and after the function has completed
;;> evaluation.  If a predicate returns \scheme{#f}, then raise an exception
;;> noting a postcondition violation with the irritants being the expression


@@ 82,11 74,14 @@
;;> fails.  As such, it is recommended to have contracts sorted from most
;;> general to most specific.
;;>
;;> A continuation captured within the function will include the
;;> postcondition checks.
;;>
;;> \bold{Example:}
;;>
;;> \schemeblock{
;;>   (define add-map
;;>     (lambda-contract (add-map . lists)
;;>     (lambda-contract lists
;;>       (pre (every list? lists)
;;>            (>= (length lists) 2)
;;>            (apply = (map length lists)))


@@ 126,7 121,7 @@
     (lambda formals e1 e2 ...))))

;;> Define a top-level function binding as with \scheme{define}'s "defun"
;;> syntax, however use \scheme{lambda-contract} instead of a regular lambda.
;;> syntax, with the addition of precondition and/or postcondition contracts.
;;>
;;> The semantics of the pre- and post-conditions is equivalent to
;;> \scheme{define-lambda.}


@@ 142,7 137,7 @@
;;>           (lambda (ret) (= (length ret) (length (car lists)))))
;;>     (apply map + lists))
;;> }
;;> The above is equivalent to:
;;> is equivalent to:
;;> \schemeblock{
;;>   (define add-map
;;>     (lambda-contract lists

M contracts.sld => contracts.sld +7 -1
@@ 4,7 4,13 @@
;;; SPDX-License-Identifier: MPL-2.0
;;; Home Page: <https://git.sr.ht/~nytpu/dbc-scheme>

;;> TODO
;;> Design-by-Contracts for R7RS Scheme.
;;>
;;> This adds functionality to add pre- and post-condition contracts to
;;> functions, in a manner similar to
;;> \hyperlink[https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html]{Ada's subprogram contracts}.
;;>
;;> \bold{TODO:} Add type contracts for records and/or atoms.
;;>
;;> View additional details at the
;;> \hyperlink[https://git.sr.ht/~nytpu/dbc-scheme]{project's repository}.