source: project/release/5/simple-contracts/tags/1.0/simple-contracts.scm @ 37484

Last change on this file since 37484 was 37484, checked in by juergen, 19 months ago

simple-contracts 1.0 ported from chicken-4

File size: 16.3 KB
Line 
1; Author: Juergen Lorenz ; ju (at) jugilo (dot) de
2;
3; Copyright (c) 2016-2019, Juergen Lorenz
4; All rights reserved.
5;
6; Redistribution and use in source and binary forms, with or without
7; modification, are permitted provided that the following conditions are
8; met:
9;
10; Redistributions of source code must retain the above copyright
11; notice, this list of conditions and the following dispasser.
12;
13; Redistributions in binary form must reproduce the above copyright
14; notice, this list of conditions and the following dispasser in the
15; documentation and/or other materials provided with the distribution.
16;
17; Neither the name of the author nor the names of its contributors may be
18; used to endorse or promote products derived from this software without
19; specific prior written permission.
20;
21; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
22; IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
23; TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
24; PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
25; HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
26; SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
27; TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
28; PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
29; LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
30; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
31; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
32
33#|[
34This is my third attempt to implement Bertrand Meyer's Design by
35contract in Chicken. The other two, contracts and dbc are now considered
36obsolete.
37We enhance arguments and return values of lambda-expressions by pre- and
38postconditions respectively, thus marking a clear distinction between
39the duties of suppliers and clients. If the arguments of a procedure
40call pass the preconditions and a result-exception is raised, then the
41supplier is to blame. On the other hand, if a argument-exception is raised
42when a procedure-call is issued, then the client has violenced its
43duties and the supplier is not even forced to do anything at all. In
44other words, the supplier can safely assume a procedure is called
45with correct arguments, he or she need not and should not check them
46again.
47
48Off course, pre- and postconditions must be stored in the procedure
49itself and a representation of them must be exportable, so that both
50parties of the contract know their duties. Here is the syntax of
51xdefine, a macro to implement queries, i.e. routines without state
52changes.
53
54(xdefine ((r r? ...) .. name (a a? ...) ...) xpr ....)
55or -- with variable arguments --
56(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
57
58where name is the name of the procedure, r .. are return values with
59corresponding postconditions r? ..., a ... are fixed variables with
60preconditions a? ... and as is an optional variable argument with
61preconditions as? ...
62
63If you want to export the documentation of pre- and postcoditions, you
64can use (here without varible arguments)
65
66(xdefine ((r r? ...) .. #(name-post name name-pre) (a a? ...) ...) xpr ....)
67
68Note, that post- and precondition documentation is placed next to
69the corresponding conditions.
70
71xdefine is implemented with xlambda, whose syntax --for variable
72argument lists -- is
73
74(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
75
76where <- separates the return values from the arguments. These
77expressions can be bound via define or define-values to export the
78documentation as well. But note that in the latter case the routine must
79be named first, of course, so that we have
80
81(define-values (proc proc-pre proc-post) (xlambda ...))
82
83For state-changing routines, so called commands, xlambda can be defined
84on top of a let, thus supplying state.
85
86To make postcondition-checking easy and command-chaining possible,
87commands should return values as well, namely the changed state
88variables after and before the change, for example
89
90(let ((state ...))
91  (xlambda ((new new? ...) (old old? ...)
92            <-
93            (a a? ...) ...) | (a a? ...) ... as as? ...)
94            xpr ....)
95
96So one can check, if the state change did what it should have done.
97
98Note, that a parameter, contract-check-level, is supplied, so that one
99can always control what to check, nothing, only preconditions or pre-
100and postconditions. Only precondition check is the default.
101
102]|#
103
104(module simple-contracts
105  (simple-contracts xlambda xdefine contract-check-level)
106
107(import scheme 
108        (only (chicken base)
109              define-inline signum make-parameter
110              case-lambda error print)
111        (only checks <<< >>> true? false?))
112
113(import-for-syntax (only (chicken base) receive))
114
115;;; (contract-check-level arg ..)
116;;; -----------------------------
117;;; parameter
118(define contract-check-level
119  (make-parameter 0
120                  (lambda (x)
121                   (if (and (integer? x)
122                            (exact? x))
123                     (signum x)
124                     0))))
125
126;;; (define-er-macro (name form rename compare?) xpr . xprs)
127;;; --------------------------------------------------------
128(define-syntax define-er-macro
129  (syntax-rules ()
130    ((_ (name form rename compare?) xpr . xprs)
131     (define-syntax name
132       (er-macro-transformer
133         (lambda (form rename compare?) xpr . xprs))))))
134
135;;; (define-ir-macro (name form inject compare?) xpr . xprs)
136;;; --------------------------------------------------------
137(define-syntax define-ir-macro
138  (syntax-rules ()
139    ((_ (name form inject compare?) xpr . xprs)
140     (define-syntax name
141       (ir-macro-transformer
142         (lambda (form inject compare?) xpr . xprs))))))
143
144;;; TODO: replace proc and cons by contracts
145;;;(preconditions proc pre post)
146;;;(postconditions proc pre post)
147;;; -----------------------------
148;;; to be used in call-with-values
149(define-inline (preconditions proc pre post) pre)
150(define-inline (postconditions proc pre post) post)
151
152;;; dbc for procedures
153;;; ==================
154;;; old version, used in new version below
155;;; (xlambda [k] ((r1 r1? ...) ...(rk rk? ...)
156;;;               (x x? ...) ... xs xs? ...)
157;;;   xpr ....)
158;;; -------------------------------------------
159;;; contract-handling lambda:
160;;; k -- if provided -- is the number of return values r1 ... rk,
161;;; 1 otherwise,
162;;; the following predicates naming the corresponding postconditions,
163;;; x ... are the fixed arguments, xs the optional variable arguments,
164;;; the following predicates naming the corresponding preconditions.
165(define-ir-macro (xlambda% form inject compare?)
166;(define-ir-macro (xlambda form inject compare?)
167  (let ((multi? (integer? (cadr form))))
168    (let ((k (if multi? (cadr form) 1))
169          (header (if multi?
170                    (caddr form)
171                    (cadr form)))
172          (xpr (if multi?
173                 (cadddr form)
174                 (caddr form)))
175          (xprs (if multi?
176                  (cddddr form)
177                  (cdddr form)))
178          )
179      (receive (xargs returns)
180        (let loop ((n 0) (tail header) (head '()))
181          (if (= n k)
182            (values tail (reverse head))
183            (loop (+ n 1) (cdr tail) (cons (car tail) head))))
184        (receive (xhead xrest)
185          (let loop ((tail xargs) (head '()))
186            (cond
187              ((null? tail)
188               (values (reverse head) tail))
189              ((symbol? (car tail))
190               (values (reverse head) tail))
191              (else
192                (loop (cdr tail) (cons (car tail) head)))))
193          (let ((fargs (map car xhead))
194                (vargs (if (null? xrest)
195                         '()
196                         (car xrest)))
197                ;(loc (inject 'xlambda%)))
198                (loc (inject 'xlambda)))
199            (let* (
200              ;; no checks
201              (proc `(lambda (,@fargs ,@vargs)
202                       ,xpr ,@xprs))
203              ;; check preconditions
204              (xproc 
205                (if (null? xrest)
206                  ;; no dotted argument
207                  `(lambda (,@fargs)
208                     (apply ,proc
209                            (list ,@(map (lambda (x c)
210                                           `(<<< ',loc ,x ,@c))
211                                         (map car xhead)
212                                         (map cdr xhead)))))
213                  ;; with dotted argument
214                  `(lambda (,@fargs ,@vargs)
215                     (apply ,proc
216                            (append
217                              (list ,@(map (lambda (x c)
218                                             `(<<< ',loc ,x ,@c))
219                                           (map car xhead)
220                                           (map cdr xhead)))
221                              (map (lambda (y)
222                                     (<<< ',loc y ,@(cdr xrest)))
223                                   ,vargs))))))
224              ;; check postconditions
225              (xxproc
226                (let ((args->vals
227                        (lambda (fargs vargs)
228                          (if (null? vargs)
229                              `(list ,@fargs)
230                              `(append (list ,@fargs) ,vargs)))))
231                  (if (null? (cdr returns))
232                    ;; only one returned value
233                    `(lambda (,@fargs ,@vargs)
234                       (>>> ',loc (apply ,xproc
235                                         ,(args->vals fargs vargs))
236                                  ;,@;(cons `',(caar returns)
237                                  ;  ;      (cdar returns))))
238                                  ;  (car returns)))
239                                  ,@(cdar returns)))
240                    ;; multiple returned values
241                    `(lambda (,@fargs ,@vargs)
242                       (call-with-values
243                         (lambda ()
244                           (apply ,xproc ,(args->vals fargs vargs)))
245                         (lambda ,(map car returns)
246                           (values ,@(map (lambda (r)
247                                            `(>>> ',loc ;,@r))
248                                              ,@;(cons (car r)
249                                                ;      (cons `',(car r)
250                                                ;            (cdr r)))))
251                                                r))
252                                          returns))))))))
253              )
254              `(values
255                  (case (contract-check-level)
256                     ((-1) ,proc)
257                     ((0)  ,xproc)
258                     ((+1) ,xxproc))
259                 ;; preconditions
260                 ',(append
261                     (map (lambda (x)
262                            `(,(car x) ,@(cdr x)))
263                          xhead)
264                     (if (null? xrest)
265                       '()
266                       `(,(car xrest) ,@(cdr xrest))))
267                 ;; postconditions
268                 ',(if (null? (cdr returns)) ; one return value
269                       ;(symbol? (car returns))
270                     (let ((returns (car returns)))
271                       `(,(car returns) ,@(cdr returns)))
272                     (map (lambda (x)
273                            `(,(car x) ,@(cdr x)))
274                          returns))
275                 ))))))))
276
277;;; new version:
278;;; (xlambda ((r r? ...) .. <- (x x? ...) ...) xpr ....)
279;;; or
280;;; (xlambda ((r r? ...) .. <- (x x? ...) ... xs xs? ...) xpr ....)
281;;; or old versions (deprecated):
282;;; (xlambda k ((r1 r1? ...) ...(rk rk? ...)
283;;;             (x x? ...) ... ) xpr ....)
284;;; (xlambda k ((r1 r1? ...) ... (rk rk? ...)
285;;;             (x x? ...) ... xs xs? ...) xpr ....)
286;;; (xlambda ((r r? ...) (x x? ...) ... ) xpr ....)
287;;; (xlambda ((r r? ...) (x x? ...) ... xs xs? ...) xpr ....)
288;;; --------------------------------------------------------
289(define-er-macro (xlambda form rename compare?)
290  (let* ((k (cadr form)) (iform (if (integer? k)
291                                  (cddr form)
292                                  (cdr form))))
293    (let ((header (car iform)) (body (cdr iform))
294          (%xlambda% (rename 'xlambda%)) (%<- (rename '<-)))
295      (if (integer? k)
296        `(,%xlambda% ,k ,header ,@body)
297        (receive (results args)
298          (let loop ((header header) (results '()))
299            (cond
300              ((null? header) ; no <- symbol
301               (let ((header (reverse results)))
302                 (values (list (car header)) (cdr header))))
303              ((compare? (car header) %<-)
304               (values (reverse results) (cdr header)))
305              (else
306                (loop (cdr header) (cons (car header) results)))))
307          `(,%xlambda% ,(length results) (,@results ,@args) ,@body))))))
308
309;;; (xdefine ((r r? ...) .. name (x x? ...) ...) xpr ....)
310;;; or
311;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ...) xpr ....)
312;;; or
313;;; (xdefine ((r r? ...) .. name (x x? ...) ... xs xs? ...) xpr ....)
314;;; or
315;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ... xs xs? ...) xpr ....)
316;;; -----------------------------------------------------------------------------
317;;; defines name -- and possibly post- and precondition documentation -- as a
318;;; contract-checked procedure with postconditions named r checked by
319;;; predicates r? ... and preconditions x ... xs .. checked by x? ...
320;;; and xs? ...
321(define-er-macro (xdefine form rename compare?)
322  (let ((header (cadr form))
323        (xpr (caddr form))
324        (xprs (cdddr form))
325        (%<- (rename '<-))
326        (%define (rename 'define))
327        (%xlambda (rename 'xlambda))
328        (%define-values (rename 'define-values)))
329    (receive (posts names pres)
330      (let loop ((tail header) (head '()))
331        (if (or (symbol? (car tail)) (vector? (car tail)))
332          (values (reverse head) (car tail) (cdr tail))
333          (loop (cdr tail) (cons (car tail) head))))
334      (if (symbol? names)
335        `(,%define ,names
336                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
337        `(,%define-values ,(list (vector-ref names 1) ; name
338                                 (vector-ref names 2) ; pres
339                                 (vector-ref names 0)); posts
340                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
341        ))))
342
343;;; (simple-contracts sym ..)
344;;; -------------------------
345;;; documentation procedure
346(define simple-contracts
347  (let ((als '(
348    (simple-contracts
349      procedure:
350      (simple-contracts sym ..)
351      "documentation procedure")
352    (contract-check-level
353      parameter:
354      (contract-check-level n ..)
355      "no contract checks if n is -1"
356      "only precondition checks if n is 0, the default"
357      "pre- and postcondition checks if n is +1")
358    (xdefine
359      macro:
360      (xdefine ((r r? ...) .. name (a a? ...) ...) xpr ....)
361      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ...) xpr ....)
362      (xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
363      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as? ...) xpr ....)
364      "contract guarded version of define for procedures, where"
365      "name is the name of the procedure, post and pre"
366      "the documentations of the pre- and postconditions respectively"
367      "r ... are return values with corresponding postcondition r?"
368      "a ... are fixed arguments with preconditions a? ..."
369      "as is an optional variable argument with preconditions as? ..."
370      "xpr starts the body")
371    (xlambda
372      macro:
373      (xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ...)
374      (xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ...)
375      "contract guarded version of lambda, where"
376      "<- separates returned values r .. from arguments"
377      "r? ... are their corresponding postconditions"
378      "a ... are fixed arguments with preconditions a? ..."
379      "as is an optional variable argument with preconditions as? ..."
380      "xpr starts the body"
381      "procedures with state change should return new and old versions"
382      "of state variables before the state change")
383    )))
384    (case-lambda
385      (()
386       (map car als))
387      ((sym)
388       (let ((pair (assq sym als)))
389         (if pair
390           (for-each print (cdr pair))
391           (error "Not in list"
392                  sym
393                  (map car als))))))))
394
395) ; module simple-contracts
396
397;(import simple-contracts simple-tests)
398;  (pe '
399;     (xlambda ((result integer? odd?)
400;               <-
401;               (x integer? odd?) (y integer? even?) ys integer? even?)
402;       (apply + x y ys)))
Note: See TracBrowser for help on using the repository browser.