Changeset 37488 in project


Ignore:
Timestamp:
03/29/19 18:08:01 (12 months ago)
Author:
juergen
Message:
 
Location:
wiki
Files:
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • wiki/explicit-renaming-macros

    r34845 r37488  
    201201
    202202And here is the much easier solution with define-er-macro from the
    203 basic-macros egg.
     203procedural-macros egg.
    204204
    205205<enscript highlight="scheme">
     
    279279automatically with explicit- and implicit-renaming-macros as well?
    280280
    281 Yes, there is. You can use the bind macro from the basic-macros module.
     281Yes, there is. You can use the bind macro from the bindings module.
    282282It's a version of destructuring-bind of Common Lisp.
    283283Using it you can replace the let above
     
    290290
    291291<enscript highlight="scheme">
     292(import-for-syntax (only bindings bind))
    292293(bind (_ x y) form ...)
    293294</enscript>
     
    300301bind, but what about renaming/injecting and additional keywords?
    301302
    302 Well, the procedural-macros module, which is written on top of
    303 basic-macros, will help with solving these problems.  For example, we've
    304 provided a procedural variant of syntax-rules, named macro-rules, which
    305 cares for all three arguments of the macro-transformer, and -- based on
    306 it -- a hygienic version of define-macro.
     303Well, the procedural-macros module, will help with solving these
     304problems.  For example, we've provided a procedural variant of
     305syntax-rules, named macro-rules, which cares for all three arguments of
     306the macro-transformer, and -- based on it -- a hygienic version of
     307define-macro.
    307308
    308309<enscript highlight="scheme">
     
    319320
    320321<enscript highlight="scheme">
     322(import-for-syntax (only procedural-macros macro-rules))
    321323(define-syntax vif
    322324  (macro-rules (then else)
     
    333335For details see
    334336
    335 [[/eggref/4/basic-macros|basic-macros]]
    336 [[/eggref/4/procedural-macros|procedural-macros]]
     337[[/eggref/5/procedural-macros|procedural-macros]]
    337338
    338339Procedural macros are really great ...
     
    354355
    355356Nov 01, 2017
     357
     358== and again for chicken-5
     359
     360Mar 29, 2019
     361
  • wiki/simple-design-by-contract

    r37378 r37488  
    5050implement Design by Contract in CHICKEN Scheme.
    5151
    52 == The dbc module
     52== The simple-contracts module
    5353
    54 This egg is an attempt, to bring DbC to CHICKEN Scheme. A module written
    55 in this style - let's call it "example" in this turorial - has to import
    56 dbc. Its body should be enclosed in
     54This egg is my third attempt, to bring DbC to CHICKEN Scheme. It only
     55considers procedures, not macros. And it assumes, that the supplier code
     56helps to check postconditions in case of commands. Hence, not only
     57queries but commands as well return results, namely the state before and
     58after a state change. So this change can be checked.
    5759
    58 <enscript highlight="scheme">
    59 (init-dbc)
    60 ...
    61 (exit-dbc-with example)
     60Besides the parameter contract-check-level, which sets the level to
     61-1, 0, or 1 respectively and according to this level, nothing, only
     62preconditions or pre- and postconditions respectively are checked,
     63there are in essence two macros xdefine and xlambda. For queries,
     64xdefine can be used, for commands xlambda must be used.
     65
     66Note, that in the former case, the procedure name or a vector with the
     67name and the post- and preconditions separate results from arguments,
     68in the latter case, this separation is done by the special symbol <-.
     69As in C the results are to the left, the arguments to the right of this
     70separator. The argument- and result-names are followed by predicates
     71and parenthesized, except rest parameters, where the parentheses are
     72skipped. Their predicates check each argument of the rest parameter.
     73
     74<enscript highlight=scheme>
     75
     76(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)
     77(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
     78
    6279</enscript>
    6380
    64 which guarantees, that documentation is automatically collected and
    65 saved in a dipatcher routine, by convention the module's name. Calling
    66 the dispatcher with no arguments returns a list of the exported symbols,
    67 with one of these symbols, it returns the symbol's documentation and
    68 called with a string it saves the skeleton of wiki-documentation in a
    69 file with the string's name.
     81<enscript highlight=scheme>
    7082
    71 This automatic documentation is essential for DbC, after all a contract
    72 without a treaty, i.e. the "small print" is useless, since both parties
    73 need to know and accept their rights and duties.
     83(xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ....)
     84(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
    7485
    75 === The syntax
     86=== Examples
    7687
    77 Let's start with the interface. We'll package the needed macros and
    78 procedures into a CHICKEN module called dbc. The fundamental macros are
    79 called
    80 
    81 * contract (for functions),
    82 * command-contract (for commands) and
    83 * macro-contract (for low-level macros).
    84 
    85 Their syntax is similar to the syntax of syntax-rules as explained
    86 below.
    87 
    88 There are no contracts for high-level macros, because the pattern
    89 matching process of syntax-rules can be considered as precondition
    90 checking. After all, macros are evaluated at compile time, i.e. before
    91 runtime. Hence they have no access to an expression's value, they treat
    92 expressions as literal lists.  Hence preconditions can only check, if
    93 those expressions match some patterns .... But something should be done
    94 to document the accepted patterns, since syntax-rules' error messages
    95 
    96   during expansion of (name ...) - no rule matches form: (name ...)
    97 
    98 don't help without documentation:
    99 
    100 * push-contract!
    101 
    102 can provide the necessary documentation by hand.
    103 
    104 These contract macros are used with
    105 
    106 <enscript highlight="scheme">
    107 (define-with-contract contract-expression procedure)
    10888</enscript>
    10989
    110 for both procedure types and
     90<enscript highlight=scheme>
    11191
    112 <enscript highlight="scheme">
    113 (define-macro-with-contract
    114    macro-contract-expression
    115    macro-transformer-expression).
    116 </enscript>
     92(import simple-contracts checks)
    11793
    118 Above I said, that the syntax of contract expressions is similar to the
    119 syntax of syntax-rules
     94(define-values (counter! counter)
     95  (let ((state 0))
     96    (values
     97      (xlambda ((new (cut = <> (add1 old)))
     98                ;integer? (lambda (x) (= x (add1 old))))
     99                (old integer?)
     100                <-)
     101        (let ((old state))
     102          (set! state (add1 state))
     103          (values state old)))
     104      (xlambda ((result (cut = <> state))
     105                <-)
     106        state))))
    120107
    121 <enscript highlight="scheme">
    122 (syntax-rules (key ...) (pat0 tpl0) (pat1 tpl1) ...)
    123 </enscript>
     108(counter) ; -> 0
     109(counter!)
     110(counter)  ; -> 1
     111(counter!)
     112(counter)  ; -> 2
    124113
    125 where pat0, pat1 ... are nested lambda-lists and tpl0, tpl1, ... the
    126 templates to be generated by the macro for the first pattern matching
    127 the macro's use.
     114(define-values (push pop top)
     115  (let ((stk '()))
     116    (let (
     117          (push
     118            (xlambda ((new list? (cut equal? <> (cons arg old)))
     119                      (old list?)
     120                      <-
     121                      (arg))
     122              (let ((old stk))
     123                (set! stk (cons arg stk))
     124                (values stk old))))
     125          (pop
     126            (xlambda ((new list? (cut equal? <> (cdr old)))
     127                      (old list?)
     128                      <-)
     129              (let ((old (<<< 'pop stk (o not null?))))
     130                (set! stk (cdr stk))
     131                (values stk old))))
     132          (top
     133            (xlambda ((result) <-)
     134              (car (<<< 'top stk (o not null?)))))
     135          )
     136      (values push pop top)
     137      )))
    128138
    129 ==== Macro contracts
     139;(top) ; precondition violated
     140;(pop) ; precondition violated
     141(push 0)
     142(push 1)
     143(top) ; -> 1
     144(call-with-values (lambda () (push 2)) list) ; -> '((2 1 0) (1 0))
     145(top) ; -> 2
     146(call-with-values (lambda () (pop)) list) ; -> '((1 0) (2 1 0))
    130147
    131 A macro-contract expression changes the templates to matchers, i.e.
    132 routines which check, if the macro expansion matches some nested
    133 lambda-list and eventually some additional conditions. The matches?
    134 macro will do that job.  Moreover, the patterns pat0, pat1 ... must
    135 eventually pass some fenders to be considered a match (this is an
    136 extension well known from syntax-case macros of R6RS). And last, but
    137 not least, low-level macros might be unhygienic, and the "dirty"
    138 symbols which pollute the name-space should be documented. In sum,
    139 macro-contracts look like this, if we use pseudo-variables .. and ....
    140 (besides ellipses, ..., "repeat the pattern on the left zero or many
    141 times") to mean "repeat the pattern to the left zero or one times, or
    142 one or many times" respectively.
     148(define-values (add add-pre add-post)
     149  (xlambda ((result integer? odd? (cut = <> (apply + x y ys)))
     150            <-
     151            (x integer? odd?) (y integer? even?) ys integer? even?)
     152    (apply + x y ys)))
    143153
    144 <enscript highlight="scheme">
    145 (macro-contract hyg ... (key ...) (pat fender matcher) ....)
    146 </enscript>
    147 
    148 ==== Function contracts
    149 
    150 Functions without side effect are controlled by
    151 
    152 <enscript highlight="scheme">
    153 (contract (result ....) (pat pre post) ....)
    154 </enscript>
    155 
    156 where pat is now a lambda-list, pre a precondition and post a
    157 postcondition, pre an expression checking the pattern variables of pat,
    158 and post checking the results. Note that pre might refer to the pattern
    159 variables of pat and post additionally to result .... Since strings and
    160 symbols always return #t, you can use them as pre- or postconditions.
    161 
    162 ==== Command contracts
    163 
    164 Commands, i.e. procedures without return values, which change some
    165 state variables instead, require the most complex contract. We need to
    166 check, which state variables are changed and how. Now, commands are
    167 usually accompanied by queries, which are functions operating on a
    168 subset of the command's arguments and returning state. For example,
    169 to set-car! corresponds car, which might be used to control what
    170 set-car! changes. In sum, command-contract looks as follows
    171 
    172 <enscript highlight="scheme">
    173 (command-contract ((old new query) ....) (pat pre post) ....)
    174 </enscript>
    175 
    176 where now post operates on the pattern variables of pat as well as the
    177 old and new variables. But here remains one twist: The macro can't
    178 know, on which subset of the command's arguments the queries operate.
    179 We must tell it. In other words, the supplied queries must be lifted to
    180 command's argument list.
    181 
    182 Note that despite their similarities, there is one difference in the
    183 postconditions of these three contract macros: procedure contracts
    184 require an expression, while macro-contract requires a predicate, i.e.
    185 a function.
    186 
    187 ==== A first example
    188 
    189 Let's consider an example, a function with two return values, Euclid's
    190 integer division. Note that this contract proves, that the function
    191 does what it is supposed to do!
    192 
    193 <enscript highlight="scheme">
    194 (define-with-contract q+r
    195   (contract (q r) ; two results
    196     ((_ m n)
    197      (and ; preconditions
    198       (integer? m) (not (negative? m))
    199       (integer? n) (positive? n)
    200       (<= n m))
    201      (and ; postconditions
    202        (integer? q)
    203        (integer? r)
    204        (= (+ (* q n) r) m))))
    205   (lambda (m n)
     154(define-values (divide divide-pre divide-post)
     155  (xlambda ((q integer?)
     156            (r (lambda (x) (= (+ x (* n q)) m)))
     157            <-
     158            (m integer? (cut >= <> 0))
     159            (n integer? positive?))
    206160    (let loop ((q 0) (r m))
    207161      (if (< r n)
    208162        (values q r)
    209163        (loop (+ q 1) (- r n))))))
    210 </enscript>
    211164
    212 ==== How do all these macros work?
     165(xdefine ((result integer?)
     166          #(sum-post sum sum-pre)
     167          (a integer?) as integer?)
     168  (apply + a as))
    213169
    214 Well, it's relatively simple. The three contract expressions return a
    215 pair, consisting of its own documentation and a procedure. The latter
    216 does the actual checks. In other words, it accepts another procedure as
    217 argument and returns that very procedure with annotated checks.
    218 
    219 The two defines store the contract's documentation in a module-global
    220 variable *contracts*, supplied by init-dbc (which must therefore be
    221 unhygienic), and apply the contract's checker to its procedure argument.
    222 
    223 Isn't that a lot of checking code, you might ask, and you are right.
    224 Therefor there is a parameter,
    225 
    226 * contract-check-level
    227 
    228 with values 0, 1 and 2, meaning "no checks at all, only documentation",
    229 "check only preconditions" or "check everything" respectively. The
    230 default is 1, but in the developing phase you'll probably set it to 2.
    231 
    232 ==== How to organize your code?
    233 
    234 Typically, you'll place the raw definitions without any defenses in one
    235 module, say raw-foo, and import their names with a prefix into another
    236 one, say foo, to add the contracts to them. These prefixed names can
    237 than be used in foo's contracts as well. The second module, foo, is
    238 the one to be exported.
    239 
    240 The splitting into two modules has several advantages.
    241 First, it helps developing. Usually, you'll have an idea, what a
    242 routine should do and how to implement it. At this stage, you needn't
    243 bother about "defensing programming" or anything like this, you can add
    244 the defenses later. You can already test your ideas incrementally and
    245 see if they do what they are supposed to do.
    246 
    247 Second, you wouldn't like to check these defenses again and again in
    248 your own routines, in particular in recursive ones. It's better to do
    249 the checks only once from outside.
    250 
    251 Third, you can enhance your old modules with contracts later on
    252 without touching the code.
    253 
    254 Fourth, if you like driving without a security belt and are concerned
    255 with speed, you can import raw-foo instead of foo into client code.
    256 
    257 ==== Another example with two modules
    258 
    259 The following rather contrieved example may clarify this. The resulting
    260 module, foo, contains all three contract types.
    261 
    262 <enscript highlight="scheme">
    263 (module raw-foo (adder adder! freeze)
    264         (import scheme)
    265 
    266         (define state 0)
    267         (define (adder) state)
    268         (define (adder! n) (set! state (+ state n)))
    269         (define (freeze form inject compare?)
    270                 `(lambda () ,(cadr form)))
    271 ) ; end raw-foo
    272 </enscript>
    273 
    274 Then you define and add the contracts to the prefixed names
    275 
    276 <enscript highlight="scheme">
    277 
    278 (require-library dbc)
    279 
    280 (module foo (adder adder! freeze)
    281         (import (prefix (except raw-foo freeze) "%"))
    282         (import-for-syntax (prefix (only raw-foo freeze) "%"))
    283 
    284         (define-with-contract adder
    285                 (contract (result)
    286                         ((_) #t (number? result)))
    287                 %adder)
    288 
    289         (define-with-contract adder!
    290                 (command-contract ((old new (lambda (n) (%adder))))
    291                         ((_ n) (number? n) (= new (+ old n))))
    292                 %adder!)
    293 
    294         (define-macro-with-contract freeze
    295                 (macro-contract () ((_ x) #t (matches? (lambda () x))))
    296                 (ir-macro-transformer %freeze))
    297 ) ; end foo
    298170</enscript>
    299171
     
    302174[[/users/juergen-lorenz|Juergen Lorenz]]
    303175
    304 == Initial version
    305 
    306 Jan 15, 2013
    307 
Note: See TracChangeset for help on using the changeset viewer.