Changeset 34636 in project


Ignore:
Timestamp:
09/22/17 18:46:01 (3 months ago)
Author:
juergen
Message:

simple-contracts 1.4 docu

File:
1 edited

Legend:

Unmodified
Added
Removed
  • wiki/eggref/4/simple-contracts

    r33862 r34636  
    2222Off course, pre- and postconditions must be stored in the procedure
    2323itself and a representation of them must be exportable, so that both
    24 parties of the contract know their duties. Here is the syntax of
    25 xdefine, a macro to implement queries, i.e. routines without state
    26 changes.
     24parties of the contract know their duties.
     25
     26Here is the syntax of xdefine, a macro to implement queries, i.e.
     27routines without state changes. Two of the four versions are shown
     28below, the first with exported documentation and fixed argument list,
     29the second without documentation and variable argument list.
     30Note that the documentations, post and pre, are placed next to their
     31corresponding checks.
    2732
    2833<enscript highlight=scheme>
    29 (xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) xpr ....)
     34(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)
     35(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
    3036</enscript>
    3137
    32 where name is the name of the procedure, r ... are retrurn values with
    33 corresponding postconditions r? ..., a ... are fixed variables with
    34 preconditions a? ... and as is an optional variable argument with
    35 preconditions as? ...
    36 
    37 For state-changing routines, so called commands, xlambda must
    38 be used. The syntax is
     38Here name is the name of the procedure, post and pre the documentation
     39of post- and preconditions,  r ... are return values with corresponding
     40postconditions r? ..., a ... are argument variables with preconditions
     41a? ... , as is the variable collecting rest arguments with
     42preconditions as? ... for each such argument and xpr starts the body.
     43
     44For state-changing routines, so called commands, mostly defined on top
     45of a let, xlambda must be used. The syntax for a fixed resp. variable
     46argument list is
    3947
    4048<enscript highlight=scheme>
    41 (xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) xpr ....)
    42 (xlambda ((r r? ...) (a a? ...) ... [as as? ...]) xpr ....)
     49(xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ....)
     50(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
    4351</enscript>
    4452
    45 where k is the number of return values, if provided, 1 otherwise.
    46 xlambda can be defined on top of a let, thus supplying state. But even
    47 those routines must return values, namely the values of state variables
    48 before a state change has taken place. So one can check, if the state
    49 change did what it should have done.
    50 
    51 Note, that a parameter, contract-check-level, is supplied, so that one
    52 can always control what to check, nothing, only preconditions or pre-
    53 and postconditions. Only precondition check is the default.
     53where <- separates the return values from the arguments. The other
     54symbols have the same meaning as in xdefine above.
     55
     56xlambda expressions return three values, the procedure itself, contract
     57checked or not, depending on the value of the contract-check-level
     58parameter, the precondition- and the postcondition-documentation in this
     59order.
     60
     61In previous versions of the library, instead of <-, you had to supply
     62the number of return values, either explicitly or implicitly, meaning
     63one. This is still working but deprecated and will propably be removed
     64in future versions.
     65 
     66Note, that even state changing routines must return values, at best the
     67values of state variables after and before a state change has taken
     68place. This makes postcondition checks and command chaining easy.
    5469
    5570=== Documentation
     
    7287==== xdefine
    7388
    74 <macro>(xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) . body)</macro>
    75 
    76 contract guarded version of define for procedures, where
    77 name is the name of the procedure
    78 r ... are return values with corresponding postcondition r?
    79 a ... are fixed arguments with preconditions a? ...
    80 as is an optional variable argument with preconditions as? ...
     89<macro>(xdefine ((r r? ...) .. name (a a? ...) ... ) xpr ....)</macro>
     90<macro>(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)</macro>
     91<macro>(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)</macro>
     92<macro>(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as?  ...) xpr ....)</macro>
     93
     94Contract guarded version of define for procedures, where
     95name is the name of the procedure,
     96post and pre document post- and preconditions
     97r ... are return values with corresponding postconditions r? ...
     98a ... are arguments with preconditions a? ...
     99as is a variable collecting rest-parameters with preconditions as? for
     100each such argument,
     101and xpr starts the body..
    81102
    82103==== xlambda
    83104
    84 <macro>(xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) . body)</macro>
    85 <macro>(xlambda ((r r? ...) (a a? ...) ... [as as? ...]) . body)</macro>
    86 
    87 contract guarded version of lambda, where
    88 k is the number of returned values r ..., if provided, 1 otherwise,
    89 r? ... their corresponding postconditions,
    90 a ... are fixed arguments with preconditions a? ...,
    91 as is an optional variable argument with preconditions as? ...
    92 
    93 procedures with state change should return old versions
    94 of state variables before the state change
     105<macro>(xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ....)</macro>
     106<macro>(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)</macro>
     107
     108where <- separates the results r with postconditions r? ... from the
     109arguments a with preconditions a? ... a rest-parameter as with
     110preconditions as? for each such argument and the body xpr .....
     111
     112Each xlambda call returns three values, the procedure proper,
     113contract-checked or not, depending on the value of contract-check-level, and
     114documentation of pre- and postconditions in this order.
     115
     116Deprecated versions of xlambda exist as well. Here k is the number of
     117returned values, if provided, one otherwise.
     118
     119<macro>(xlambda k ((r r? ...) ... (a a? ...) ... ) xpr ....)</macro>
     120<macro>(xlambda k ((r r? ...) ... (a a? ...) ... as as? ...) xpr ....)</macro>
     121<macro>(xlambda ((r r? ...) (a a? ...) ... ) xpr ....)</macro>
     122<macro>(xlambda ((r r? ...) (a a? ...) ... as as? ...) xpr ....)</macro>
     123
     124procedures with state change should return the values of state variables
     125after and before the state change.
    95126
    96127==== %%
     
    104135<macro>(pipe combination ...)</macro>
    105136
    106 sequencing curried combinations
     137sequencing curried combinations from left to right
    107138
    108139=== Requirements
     
    120151<enscript highlight=scheme>
    121152
    122 (use simple-contracts)
     153(use simple-contracts simple-exceptions)
    123154
    124155((%% list)) ; -> '()
     
    141172  (let ((state 0))
    142173    (values
    143       (xlambda 1 ((old (pipe (+ 1) (= state))))
    144         (let ((o state))
     174      (xlambda ((new (pipe (= (add1 old))))
     175                     ;integer? (pipe (= (add1 old))))
     176                     ;integer? (lambda (x) (= x (add1 old))))
     177                (old integer?)
     178                <-) ; no arguments
     179        (let ((old state))
    145180          (set! state (add1 state))
    146           o))
    147       (xlambda 1 ((result (pipe (= state))))
     181          (values state old)))
     182      (xlambda ((result (pipe (= state)))
     183                <-) ; no arguments
    148184        state))))
    149185(counter) ; -> 0
     
    153189(counter)  ; -> 2
    154190
     191(define-values (push pop top)
     192  (let ((stk '()))
     193    (let (
     194      (push
     195        (xlambda ((new list? (pipe (equal? (cons arg old))))
     196                  (old list?)
     197                  <-
     198                  (arg))
     199          (let ((old stk))
     200            (set! stk (cons arg stk))
     201            (values stk old))))
     202      (pop
     203        (xlambda ((new list? (pipe (equal? (cdr old))))
     204                  (old list?)
     205                  <-)
     206          (let ((old (<< stk 'pop (pipe (null?) (not)))))
     207            (set! stk (cdr stk))
     208            (values stk old))))
     209      (top
     210        (xlambda ((result) <-)
     211          (car (<< stk 'top (pipe (null?) (not))))))
     212      )
     213      (values push pop top)
     214      )))
     215;(top) ; precondition violated
     216;(pop) ; precondition violated
     217(push 0)
     218(push 1)
     219(top) ; -> 1
     220(call-with-values (lambda () (push 2)) list) ; -> '((2 1 0) (1 0))
     221(top) ; -> 2
     222(call-with-values (lambda () (pop)) list) ; -> '((1 0) (2 1 0))
     223
    155224(define-values (add add-pre add-post)
    156225  (xlambda ((result integer? odd? (pipe (= (apply + x y ys))))
     226            <-
    157227            (x integer? odd?) (y integer? even?) ys integer? even?)
    158228    (apply + x y ys)))
    159229(add 1 2 4 6) ; -> 13
    160230(condition-case (add 1 2 3) ((exn arguments) #f)) ; -> #f
    161 add-pre
    162  ; -> '((x (conjoin integer? odd?))
    163         (y (conjoin integer? even?))
    164         ys (conjoin integer?  even?))
     231add-pre ; -> '((x (conjoin integer? odd?))
     232               (y (conjoin integer? even?))
     233               ys (conjoin integer?  even?))
    165234add-post
    166235 ; -> '(result (conjoin integer? odd? (pipe (= (apply + x y ys)))))
     
    168237(define wrong-add
    169238  (xlambda ((result integer? even?)
     239            <-
    170240            (x integer? odd?) xs integer?  even?)
    171241    (apply + x xs)))
    172242(condition-case (wrong-add 1 2 4) ((exn results) #f)) ; -> #f
    173243
    174 (define-values (euclid euclid-pre euclid-post)
    175   (xlambda 2 ((q integer?)
    176               (r (pipe (+ (* n q))
    177                        (= m)))
    178               (m integer? (pipe (>= 0)))
    179               (n integer? positive?))
     244(define-values (divide divide-pre divide-post)
     245  (xlambda ((q integer?)
     246            (r (pipe (+ (* n q))
     247                     (= m)))
     248            <-
     249            (m integer? (pipe (>= 0)))
     250            (n integer? positive?))
    180251    (let loop ((q 0) (r m))
    181252      (if (< r n)
    182253        (values q r)
    183254        (loop (+ q 1) (- r n))))))
    184 (call-with-values
    185   (lambda () (euclid 385 25))
    186   list)
    187   ; -> '(15 10)
    188 euclid-pre
    189  ; - > '((m (conjoin integer? (pipe (>= 0))))
    190          (n (conjoin integer? positive?)))
    191 euclid-post
    192  ; -> '((q integer?)
    193         (r (pipe (+ (* n q)) (= m))))
    194 
    195 (xdefine ((result integer?) sum (a integer?) as integer?)
     255  (call-with-values
     256    (lambda () (divide 385 25))
     257    list) ;-> '(15 10)
     258divide-pre ; -> '((m (conjoin integer? (pipe (>= 0))))
     259                  (n (conjoin integer? positive?)))
     260divide-post ; -> '((q integer?)
     261                   (r (pipe (+ (* n q)) (= m))))
     262 
     263
     264(xdefine ((result integer?) #(sum-post sum sum-pre) (a integer?) as integer?)
    196265  (apply + a as))
    197266(sum 1 2 3) ; -> 6
     
    206275== Last update
    207276
    208 Feb 17, 2017
     277Sep 22, 2017
    209278
    210279== Author
     
    214283== License
    215284
    216  Copyright (c) 2011-2016, Juergen Lorenz
     285 Copyright (c) 2011-2017, Juergen Lorenz
    217286 All rights reserved.
    218287
     
    244313
    245314== Version History
     315; 1.4 : syntax changes for xlambda and xdefine
    246316; 1.3.1 : dependency on simple-exceptions updated
    247317; 1.3 : error-messages improved
Note: See TracChangeset for help on using the changeset viewer.