Changeset 31097 in project for wiki/eggref/4/skiplists


Ignore:
Timestamp:
07/07/14 23:56:35 (6 years ago)
Author:
juergen
Message:

skiplists docu beautified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • wiki/eggref/4/skiplists

    r30431 r31097  
    7272
    7373<enscript highlight=scheme>
    74 
    75 (_ x y)
     74(dups x y)
    7675requires (and ((skiplist-item? sls) x) ((skiplist-item? sls) y))
    7776ensures  (fx= result 0)
    78 
    7977</enscript>
    8078
     
    8886
    8987<enscript highlight=scheme>
    90 
    91 (_ width max-height item? order . orders)
     88(skiplist width max-height item? order . orders)
    9289requires (and (fixnum? width)
    9390              (fx> width 1)
     
    10097              ((list-of? procedure?) orders)
    10198              " like order, last one might be dups")
    102 ensures  (%skiplist? result)
    103 
    104 (_ max-height item? order . orders)
     99ensures  (skiplist? result)
     100
     101(skiplist max-height item? order . orders)
    105102"width defaults to 2"
    106103requires (and (fixnum? max-height)
     
    112109              ((list-of? procedure?) orders)
    113110              " like order, last one might be dups")
    114 ensures  (%skiplist? result)
    115 
    116 (_ item? order . orders)
     111ensures  (skiplist? result)
     112
     113(skiplist item? order . orders)
    117114"width defaults to 2, max-height to 10"
    118115requires (and (procedure? item?)
     
    122119              ((list-of? procedure?) orders)
    123120              " like order, last one might be dups")
    124 ensures  (%skiplist? result)
    125 
     121ensures  (skiplist? result)
    126122</enscript>
    127123
     
    133129
    134130<enscript highlight=scheme>
    135 
    136 (_ sls)
    137 requires (%skiplist? sls)
    138 ensures  ((list-of? (%skiplist-item? sls)) result)
    139 
    140 (_ sls level)
    141 requires (and (%skiplist? sls)
     131(skiplist->list sls)
     132requires (skiplist? sls)
     133ensures  ((list-of? (skiplist-item? sls)) result)
     134
     135(skiplist->list sls level)
     136requires (and (skiplist? sls)
    142137              (fixnum? level)
    143138              (fx<= 0 level)
    144               (fx< level (%skiplist-height sls)))
    145 ensures  ((list-of? (%skiplist-item? sls)) result)
    146 
     139              (fx< level (skiplist-height sls)))
     140ensures  ((list-of? (skiplist-item? sls)) result)
    147141</enscript>
    148142
     
    151145<procedure>(skiplist-clear! sls)</procedure>
    152146
    153 command ((oldcount newcount %skiplist-count) (oldheight newheight %skiplist-height))
    154 
    155 <enscript highlight=scheme>
    156 
    157 (_ sls)
    158 requires (%skiplist? sls)
     147command ((oldcount newcount skiplist-count) (oldheight newheight skiplist-height))
     148
     149<enscript highlight=scheme>
     150(skiplist-clear! sls)
     151requires (skiplist? sls)
    159152ensures  (and (fx= 0 newcount) (fx= 1 newheight))
    160 
    161153</enscript>
    162154
     
    168160
    169161<enscript highlight=scheme>
    170 
    171 (_ sls)
    172 requires (%skiplist? sls)
     162(skiplist-compare sls)
     163requires (skiplist? sls)
    173164ensures  (and (procedure? result) "(fixnum? (result x y))")
    174 
    175165</enscript>
    176166
     
    182172
    183173<enscript highlight=scheme>
    184 
    185 (_ sls)
    186 requires (%skiplist? sls)
     174(skiplist-count sls)
     175requires (skiplist? sls)
    187176ensures  (and (fixnum? result) (fx>= result 0))
    188 
    189177</enscript>
    190178
     
    196184
    197185<enscript highlight=scheme>
    198 
    199 (_ sls)
    200 requires (%skiplist? sls)
     186(skiplist-dups? sls)
     187requires (skiplist? sls)
    201188ensures  (boolean? result)
    202 
    203189</enscript>
    204190
     
    210196
    211197<enscript highlight=scheme>
    212 
    213 (_ sls ok?)
    214 requires (and (%skiplist? sls) (procedure? ok?) "(boolean? (ok? x))")
    215 ensures  (%skiplist? result)
    216 
     198(skiplist-filter sls ok?)
     199requires (and (skiplist? sls) (procedure? ok?) "(boolean? (ok? x))")
     200ensures  (skiplist? result)
    217201</enscript>
    218202
     
    224208
    225209<enscript highlight=scheme>
    226 
    227 (_ sls proc)
    228 requires (and (%skiplist? sls) (procedure? proc))
     210(skiplist-for-each sls proc)
     211requires (and (skiplist? sls) (procedure? proc))
    229212ensures  new
    230 
    231213</enscript>
    232214
     
    238220
    239221<enscript highlight=scheme>
    240 
    241 (_ sls)
    242 requires (%skiplist? sls)
    243 ensures  ((list-of? (%skiplist-item? sls)) result)
    244 
     222(skiplist-found sls)
     223requires (skiplist? sls)
     224ensures  ((list-of? (skiplist-item? sls)) result)
    245225</enscript>
    246226
     
    252232
    253233<enscript highlight=scheme>
    254 
    255 (_ sls item)
    256 requires (and (%skiplist? sls) ((%skiplist-item? sls) item))
     234(skiplist-found? sls item)
     235requires (and (skiplist? sls) ((skiplist-item? sls) item))
    257236ensures  (boolean? result)
    258 
    259237</enscript>
    260238
     
    266244
    267245<enscript highlight=scheme>
    268 
    269 (_ sls)
    270 requires (%skiplist? sls)
     246(skiplist-height sls)
     247requires (skiplist? sls)
    271248ensures  (and (fixnum? result) (fx> result 0))
    272 
    273249</enscript>
    274250
     
    277253<procedure>(skiplist-insert! sls item . items)</procedure>
    278254
    279 command ((oldcount newcount (lambda (sls . items) (%skiplist-count sls)))
     255command ((oldcount newcount (lambda (sls . items) (skiplist-count sls)))
    280256         (oldfound newfound (lambda (sls . items)
    281                               (%skiplist-search! sls (car items))
    282                               (%skiplist-found sls))))
    283 
    284 <enscript highlight=scheme>
    285 
    286 (_ sls item . items)
    287 requires (and (%skiplist? sls)
    288               ((list-of? (%skiplist-item? sls)) (cons item items)))
     257                              (skiplist-search! sls (car items))
     258                              (skiplist-found sls))))
     259
     260<enscript highlight=scheme>
     261(skiplist-insert! sls item . items)
     262requires (and (skiplist? sls)
     263              ((list-of? (skiplist-item? sls)) (cons item items)))
    289264ensures  (and (fx>= newcount oldcount) (member item newfound))
    290 
    291265</enscript>
    292266
     
    298272
    299273<enscript highlight=scheme>
    300 
    301 (_ sls)
    302 requires (%skiplist? sls)
     274(skiplist-item? sls)
     275requires (skiplist? sls)
    303276ensures  (procedure? result)
    304 
    305277</enscript>
    306278
    307279==== skiplist-map
    308280
    309 <procedure>(or (skiplist-map sls fn)
    310                (skiplist-map sls fn order . orders)
    311                (skiplist-map sls fn width)
    312                (skiplist-map sls fn width order . orders))
    313 </procedure>
    314 
    315 function (result)
    316 
    317 <enscript highlight=scheme>
    318 
    319 (_ sls fn)
    320 requires (and (%skiplist? sls)
     281<procedure>(skiplist-map sls fn)</procedure>
     282<procedure>(skiplist-map sls fn order . orders)</procedure>
     283<procedure>(skiplist-map sls fn width)</procedure>
     284<procedure>(skiplist-map sls fn width order . orders)</procedure>
     285
     286function (result)
     287
     288<enscript highlight=scheme>
     289(skiplist-map sls fn)
     290requires (and (skiplist? sls)
    321291              (procedure? fn)
    322292              "((skiplist-item? sls) (fn x))")
    323 ensures  (%skiplist? result)
    324 
    325 (_ sls fn item? order . orders)
    326 requires (and (%skiplist? sls)
     293ensures  (skiplist? result)
     294
     295(skiplist-map sls fn item? order . orders)
     296requires (and (skiplist? sls)
    327297              (procedure? fn)
    328298              (procedure? item?)
    329299              (((list-of? procedure?) (cons order orders))))
    330 ensures  (%skiplist? result)
    331 
     300ensures  (skiplist? result)
    332301</enscript>
    333302
     
    339308
    340309<enscript highlight=scheme>
    341 
    342 (_ sls)
    343 requires (%skiplist? sls)
    344 ensures  ((list-of? (%skiplist-item? sls)) result)
    345 
     310(skiplist-max sls)
     311requires (skiplist? sls)
     312ensures  ((list-of? (skiplist-item? sls)) result)
    346313</enscript>
    347314
     
    353320
    354321<enscript highlight=scheme>
    355 
    356 (_ sls)
    357 requires (%skiplist? sls)
     322(skiplist-max-height sls)
     323requires (skiplist? sls)
    358324ensures  (and (fixnum? result) (fx> result 1))
    359 
    360325</enscript>
    361326
     
    367332
    368333<enscript highlight=scheme>
    369 
    370 (_ sls)
    371 requires (%skiplist? sls)
    372 ensures  ((list-of? (%skiplist-item? sls)) result)
    373 
     334(skiplist-min sls)
     335requires (skiplist? sls)
     336ensures  ((list-of? (skiplist-item? sls)) result)
    374337</enscript>
    375338
     
    381344
    382345<enscript highlight=scheme>
    383 
    384 (_ sls)
    385 requires (%skiplist? sls)
     346(skiplist-null? sls)
     347requires (skiplist? sls)
    386348ensures  (boolean? result)
    387 
    388349</enscript>
    389350
     
    395356
    396357<enscript highlight=scheme>
    397 
    398 (_ sls)
    399 requires (%skiplist? sls)
     358(skiplist-orders sls)
     359requires (skiplist? sls)
    400360ensures  ((list-of? procedure?) result)
    401 
    402361</enscript>
    403362
     
    407366
    408367command ((oldcount newcount (lambda (sls . items)
    409                               (%skiplist-count sls))))
    410 
    411 <enscript highlight=scheme>
    412 
    413 (_ sls item . items)
    414 requires (and (%skiplist? sls)
    415               ((list-of? (%skiplist-item? sls)) (cons item items)))
     368                              (skiplist-count sls))))
     369
     370<enscript highlight=scheme>
     371(skiplist-remove! sls item . items)
     372requires (and (skiplist? sls)
     373              ((list-of? (skiplist-item? sls)) (cons item items)))
    416374ensures  (fx<= newcount oldcount)
    417 
    418375</enscript>
    419376
     
    425382
    426383<enscript highlight=scheme>
    427 
    428 (_ sls order . orders)
    429 requires (and (%skiplist? sls)
     384(skiplist-reorder sls order . orders)
     385requires (and (skiplist? sls)
    430386              ((list-of? procedure?) (cons order orders))
    431387              "each (fixnum? (order x y))")
    432 ensures  (%skiplist? result)
    433 
     388ensures  (skiplist? result)
    434389</enscript>
    435390
     
    441396
    442397<enscript highlight=scheme>
    443 
    444 (_ sls width max-height)
    445 requires (and (%skiplist? sls) (fixnum? width) (fx> width 1)
     398(skiplist-restructure sls width max-height)
     399requires (and (skiplist? sls) (fixnum? width) (fx> width 1)
    446400              (fixnum? max-height) (fx> max-height 1))
    447 ensures  (%skiplist? result)
    448 
     401ensures  (skiplist? result)
    449402</enscript>
    450403
     
    454407
    455408command ((oldlevel newlevel (lambda (sls item)
    456                               (%skiplist-search-level sls)))
    457          (oldfound newfound (lambda (sls item) (%skiplist-found sls))))
    458 
    459 <enscript highlight=scheme>
    460 
    461 (_ sls item)
    462 requires (and (%skiplist? sls)
    463               ((%skiplist-item? sls) item))
     409                              (skiplist-search-level sls)))
     410         (oldfound newfound (lambda (sls item) (skiplist-found sls))))
     411
     412<enscript highlight=scheme>
     413(skiplist-search! sls item)
     414requires (and (skiplist? sls)
     415              ((skiplist-item? sls) item))
    464416ensures  (and (fx>= newlevel 0)
    465               (fx< newlevel (%skiplist-height sls))
    466               ((list-of? (%skiplist-item? sls)) newfound)
     417              (fx< newlevel (skiplist-height sls))
     418              ((list-of? (skiplist-item? sls)) newfound)
    467419              ((list-of? zero?)
    468                (map (lambda (x) ((%skiplist-compare sls) item x))
     420               (map (lambda (x) ((skiplist-compare sls) item x))
    469421                    newfound)))
    470 
    471422</enscript>
    472423
     
    478429
    479430<enscript highlight=scheme>
    480 
    481 (_ sls)
    482 requires (%skiplist? sls)
     431(skiplist-search-level sls)
     432requires (skiplist? sls)
    483433ensures  (and (fixnum? result) (fx>= result 0) (fx< result (skiplist-height sls)))
    484 
    485434</enscript>
    486435
     
    492441
    493442<enscript highlight=scheme>
    494 
    495 (_ sls)
    496 requires (%skiplist? sls)
     443(skiplist-width sls)
     444requires (skiplist? sls)
    497445ensures  (and (fixnum? result) (fx> result 1))
    498 
    499446</enscript>
    500447
     
    506453
    507454<enscript highlight=scheme>
    508 
    509 (_ xpr)
     455(skiplist? xpr)
    510456requires #t
    511457ensures  (boolean? result)
    512 
    513458</enscript>
    514459
Note: See TracChangeset for help on using the changeset viewer.