Changeset 31103 in project


Ignore:
Timestamp:
07/08/14 12:51:13 (6 years ago)
Author:
juergen
Message:

docu of skiplists and random-access-lists improved

Location:
wiki/eggref/4
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • wiki/eggref/4/random-access-lists

    r30140 r31103  
    2424to a given position, pos, works as follows: One starts at the highest
    2525level and follows the next link at that level adding the jump at that
    26 level to the place at that level until the ladder is less than pos but
     26level to the place at that level until the latter is less than pos but
    2727a further movement at that level would be greater or equal pos. Then
    2828one saves cursor and place and restarts the same movement process at
     
    7878<procedure>(make-ral item? . args)</procedure>
    7979
    80 function (result)
    81 
    82 <enscript highlight=scheme>
    83 
    84 (_ item? . args)
     80<enscript highlight=scheme>
     81function (result)
    8582requires (and ((list-of? (lambda (arg) (and (fixnum? arg) (fx> arg 1)))) args)
    8683              (procedure? item?) "(item? item)")
    87 ensures  (%ral? result)
    88 
     84ensures  (ral? result)
    8985</enscript>
    9086
    9187==== ral->list
    9288
    93 <procedure>(or (ral->list ls) (ral->list ls level))</procedure>
    94 
    95 function (result)
    96 
    97 <enscript highlight=scheme>
    98 
    99 (_ ls)
    100 requires (%ral? ls)
    101 ensures  ((list-of? (%ral-item? ls)) result)
    102 
    103 (_ ls level)
    104 requires (and (%ral? ls) (fixnum? level)
    105               (fx<= 0 level) (fx< level (%ral-height ls)))
    106 ensures  ((list-of? (%ral-item? ls)) result)
    107 
     89<procedure>(ral->list ls)</procedure>
     90<procedure>(ral->list ls level)</procedure>
     91
     92<enscript highlight=scheme>
     93function (result)
     94requires (and (ral? ls) (fixnum? level)
     95              (fx<= 0 level) (fx< level (ral-height ls)))
     96         ; default (fx= level 0)
     97ensures  ((list-of? (ral-item? ls)) result)
    10898</enscript>
    10999
     
    112102<procedure>(ral-add! ls item . items)</procedure>
    113103
    114 command ((oldcount newcount (lambda (ls item . items) (%ral-count ls))))
    115 
    116 <enscript highlight=scheme>
    117 
    118 (_ ls item . items)
    119 requires (and (%ral? ls) ((%ral-item? ls) item)
    120               ((list-of? (%ral-item? ls)) items))
     104<enscript highlight=scheme>
     105command ((oldcount newcount (lambda (ls item . items) (ral-count ls))))
     106requires (and (ral? ls) ((ral-item? ls) item)
     107              ((list-of? (ral-item? ls)) items))
    121108ensures  (fx= newcount (fx+ (length (cons item items)) oldcount))
    122 
    123109</enscript>
    124110
     
    127113<procedure>(ral-add-left! ls item . items)</procedure>
    128114
    129 command ((oldcount newcount (lambda (ls item . items) (%ral-count ls))))
    130 
    131 <enscript highlight=scheme>
    132 
    133 (_ ls item . items)
    134 requires (and (%ral? ls) ((%ral-item? ls) item)
    135               ((list-of? (%ral-item? ls)) items))
     115<enscript highlight=scheme>
     116command ((oldcount newcount (lambda (ls item . items) (ral-count ls))))
     117requires (and (ral? ls) ((ral-item? ls) item)
     118              ((list-of? (ral-item? ls)) items))
    136119ensures  (fx= newcount (fx+ (length (cons item items)) oldcount))
    137 
    138120</enscript>
    139121
     
    142124<procedure>(ral-clear! ls)</procedure>
    143125
    144 command ((oldcount newcount %ral-count) (oldheight newheight %ral-height))
    145 
    146 <enscript highlight=scheme>
    147 
    148 (_ ls)
    149 requires (%ral? ls)
     126<enscript highlight=scheme>
     127command ((oldcount newcount ral-count) (oldheight newheight ral-height))
     128requires (ral? ls)
    150129ensures  (and (fx= 0 newcount) (fx= 1 newheight))
    151 
    152130</enscript>
    153131
     
    156134<procedure>(ral-count ls)</procedure>
    157135
    158 function (result)
    159 
    160 <enscript highlight=scheme>
    161 
    162 (_ ls)
    163 requires (%ral? ls)
     136<enscript highlight=scheme>
     137function (result)
     138requires (ral? ls)
    164139ensures  (and (fixnum? result) (fx>= result 0))
    165 
    166140</enscript>
    167141
     
    170144<procedure>(ral-cursor-jump ls k)</procedure>
    171145
    172 function (result)
    173 
    174 <enscript highlight=scheme>
    175 
    176 (_ ls k)
    177 requires (and (%ral? ls) (fixnum? k)
    178               (fx>= k 0) (fx< k (%ral-height ls)))
     146<enscript highlight=scheme>
     147function (result)
     148requires (and (ral? ls) (fixnum? k)
     149              (fx>= k 0) (fx< k (ral-height ls)))
    179150ensures  (and (fixnum? result)
    180               (fx> result 0) (fx<= result (%ral-count ls)))
    181 
     151              (fx> result 0) (fx<= result (ral-count ls)))
    182152</enscript>
    183153
     
    186156<procedure>(ral-cursor-next ls k)</procedure>
    187157
    188 function (result)
    189 
    190 <enscript highlight=scheme>
    191 
    192 (_ ls k)
    193 requires (and (%ral? ls) (fixnum? k)
    194               (fx>= k 0) (fx< k (%ral-height ls)))
    195 ensures  (or (null? result) (%ral-node? result))
    196 
     158<enscript highlight=scheme>
     159function (result)
     160requires (and (ral? ls) (fixnum? k)
     161              (fx>= k 0) (fx< k (ral-height ls)))
     162ensures  (or (null? result) (ral-node? result))
    197163</enscript>
    198164
     
    201167<procedure>(ral-eq? ls0 ls1)</procedure>
    202168
    203 function (result)
    204 
    205 <enscript highlight=scheme>
    206 
    207 (_ ls0 ls1)
    208 requires (and (%ral? ls0) (%ral? ls1))
     169<enscript highlight=scheme>
     170function (result)
     171requires (and (ral? ls0) (ral? ls1))
    209172ensures  (boolean? result)
    210 
    211173</enscript>
    212174
     
    215177<procedure>(ral-eql? eql? ls0 ls1)</procedure>
    216178
    217 function (result)
    218 
    219 <enscript highlight=scheme>
    220 
    221 (_ eql? ls0 ls1)
     179<enscript highlight=scheme>
     180function (result)
    222181requires (and (procedure? eql?) "(eql? item0 item1)"
    223               (%ral? ls0) (%ral? ls1))
     182              (ral? ls0) (ral? ls1))
    224183ensures  (boolean? result)
    225 
    226184</enscript>
    227185
     
    230188<procedure>(ral-equal? ls0 ls1)</procedure>
    231189
    232 function (result)
    233 
    234 <enscript highlight=scheme>
    235 
    236 (_ ls0 ls1)
    237 requires (and (%ral? ls0) (%ral? ls1))
     190<enscript highlight=scheme>
     191function (result)
     192requires (and (ral? ls0) (ral? ls1))
    238193ensures  (boolean? result)
    239 
    240194</enscript>
    241195
     
    244198<procedure>(ral-eqv? ls0 ls1)</procedure>
    245199
    246 function (result)
    247 
    248 <enscript highlight=scheme>
    249 
    250 (_ ls0 ls1)
    251 requires (and (%ral? ls0) (%ral? ls1))
     200<enscript highlight=scheme>
     201function (result)
     202requires (and (ral? ls0) (ral? ls1))
    252203ensures  (boolean? result)
    253 
    254204</enscript>
    255205
     
    258208<procedure>(ral-filter ls ok?)</procedure>
    259209
    260 function (result)
    261 
    262 <enscript highlight=scheme>
    263 
    264 (_ ls ok?)
    265 requires (and (%ral? ls) (procedure? ok?) "(ok? item)")
    266 ensures  (and (%ral? result)
    267               (fx<= (%ral-count result) (%ral-count ls)))
    268 
     210<enscript highlight=scheme>
     211function (result)
     212requires (and (ral? ls) (procedure? ok?) "(ok? item)")
     213ensures  (and (ral? result)
     214              (fx<= (ral-count result) (ral-count ls)))
    269215</enscript>
    270216
     
    273219<procedure>(ral-for-each ls proc)</procedure>
    274220
     221<enscript highlight=scheme>
    275222command ((old new (constantly #t)))
    276 
    277 <enscript highlight=scheme>
    278 
    279 (_ ls proc)
    280 requires (and (%ral? ls) (procedure? proc) "(proc item)")
     223requires (and (ral? ls) (procedure? proc) "(proc item)")
    281224ensures  new
    282 
    283225</enscript>
    284226
     
    287229<procedure>(ral-from-upto ls from upto)</procedure>
    288230
    289 function (result)
    290 
    291 <enscript highlight=scheme>
    292 
    293 (_ ls from upto)
    294 requires (and (%ral? ls) (fixnum? from) (fixnum? upto)
     231<enscript highlight=scheme>
     232function (result)
     233requires (and (ral? ls) (fixnum? from) (fixnum? upto)
    295234              (fx>= from 0) (fx>= upto from)
    296               (fx<= upto (%ral-count ls)))
    297 ensures  (and (%ral? result)
    298               (fx= (%ral-count result) (fx- upto from)))
    299 
     235              (fx<= upto (ral-count ls)))
     236ensures  (and (ral? result)
     237              (fx= (ral-count result) (fx- upto from)))
    300238</enscript>
    301239
     
    304242<procedure>(ral-height ls)</procedure>
    305243
    306 function (result)
    307 
    308 <enscript highlight=scheme>
    309 
    310 (_ ls)
    311 requires (%ral? ls)
     244<enscript highlight=scheme>
     245function (result)
     246requires (ral? ls)
    312247ensures  (and (fixnum? result) (fx> result 0))
    313 
    314248</enscript>
    315249
     
    318252<procedure>(ral-insert! ls place item)</procedure>
    319253
    320 command ((oldcount newcount (lambda (ls place item) (%ral-count ls)))
    321          (olditem newitem (lambda (ls place item) (%ral-ref ls place))))
    322 
    323 <enscript highlight=scheme>
    324 
    325 (_ ls place item)
    326 requires (and (%ral? ls) ((%ral-item? ls) item)
    327               (fixnum? place) (fx>= place 0) (fx<= place (%ral-count ls)))
     254<enscript highlight=scheme>
     255command ((oldcount newcount (lambda (ls place item) (ral-count ls)))
     256         (olditem newitem (lambda (ls place item) (ral-ref ls place))))
     257requires (and (ral? ls) ((ral-item? ls) item)
     258              (fixnum? place) (fx>= place 0) (fx<= place (ral-count ls)))
    328259ensures  (and (fx= newcount (fx+ 1 oldcount)) (equal? newitem item))
    329 
    330260</enscript>
    331261
     
    334264<procedure>(ral-item? ls)</procedure>
    335265
    336 function (result)
    337 
    338 <enscript highlight=scheme>
    339 
    340 (_ ls)
    341 requires (%ral? ls)
     266<enscript highlight=scheme>
     267function (result)
     268requires (ral? ls)
    342269ensures  (procedure? result)
    343 
    344270</enscript>
    345271
     
    348274<procedure>(ral-join head tail)</procedure>
    349275
    350 function (result)
    351 
    352 <enscript highlight=scheme>
    353 
    354 (_ head tail)
    355 requires (and (%ral? head) (%ral? tail)
    356               (eq? (%ral-item? head) (%ral-item? tail)))
    357 ensures  (and (%ral? result)
    358               (fx= (%ral-count result)
    359                    (fx+ (%ral-count head) (%ral-count tail))))
    360 
     276<enscript highlight=scheme>
     277function (result)
     278requires (and (ral? head) (ral? tail)
     279              (eq? (ral-item? head) (ral-item? tail)))
     280ensures  (and (ral? result)
     281              (fx= (ral-count result)
     282                   (fx+ (ral-count head) (ral-count tail))))
    361283</enscript>
    362284
     
    365287<procedure>(ral-level ls)</procedure>
    366288
    367 function (result)
    368 
    369 <enscript highlight=scheme>
    370 
    371 (_ ls)
    372 requires (%ral? ls)
     289<enscript highlight=scheme>
     290function (result)
     291requires (ral? ls)
    373292ensures  (and (fixnum? result) (fx> result 0)
    374               (fx< result (%ral-height ls)))
    375 
     293              (fx< result (ral-height ls)))
    376294</enscript>
    377295
    378296==== ral-map
    379297
    380 <procedure>(or (ral-map ls fn) (ral-map ls fn item?))</procedure>
    381 
    382 function (result)
    383 
    384 <enscript highlight=scheme>
    385 
    386 (_ ls fn)
    387 requires (and (%ral? ls) (procedure? fn) "(fn item)")
    388 ensures  (and (%ral? result)
    389               (fx= (%ral-count result) (%ral-count ls)))
    390 
    391 (_ ls fn item?)
    392 requires (and (%ral? ls) (procedure? fn) "(fn item)"
     298<procedure>(ral-map ls fn)</procedure>
     299<procedure>(ral-map ls fn item?)</procedure>
     300
     301<enscript highlight=scheme>
     302function (result)
     303requires (and (ral? ls) (procedure? fn) "(fn item)"
    393304              (procedure? item?) "(item? item)")
    394 ensures  (and (%ral? result) (fx= (%ral-count result) (%ral-count ls))
    395               (eq? item? (%ral-item? result)))
    396 
     305         ; default (eq? item? ral-item?)
     306ensures  (and (ral? result) (fx= (ral-count result) (ral-count ls))
     307              (eq? item? (ral-item? result)))
    397308</enscript>
    398309
     
    401312<procedure>(ral-max-height ls)</procedure>
    402313
    403 function (result)
    404 
    405 <enscript highlight=scheme>
    406 
    407 (_ ls)
    408 requires (%ral? ls)
     314<enscript highlight=scheme>
     315function (result)
     316requires (ral? ls)
    409317ensures  (and (fixnum? result) (fx> result 0))
    410 
    411318</enscript>
    412319
     
    415322<procedure>(ral-node? xpr)</procedure>
    416323
    417 function (result)
    418 
    419 <enscript highlight=scheme>
    420 
    421 (_ xpr)
     324<enscript highlight=scheme>
     325function (result)
    422326requires #t
    423327ensures  (boolean? result)
    424 
    425328</enscript>
    426329
     
    429332<procedure>(ral-null? ls)</procedure>
    430333
    431 function (result)
    432 
    433 <enscript highlight=scheme>
    434 
    435 (_ ls)
    436 requires (%ral? ls)
     334<enscript highlight=scheme>
     335function (result)
     336requires (ral? ls)
    437337ensures  (boolean? result)
    438 
    439338</enscript>
    440339
     
    443342<procedure>(ral-place ls k)</procedure>
    444343
    445 function (result)
    446 
    447 <enscript highlight=scheme>
    448 
    449 (_ ls k)
    450 requires (and (%ral? ls) (fixnum? k)
    451               (fx>= k 0) (fx< k (%ral-height ls)))
     344<enscript highlight=scheme>
     345function (result)
     346requires (and (ral? ls) (fixnum? k)
     347              (fx>= k 0) (fx< k (ral-height ls)))
    452348ensures  (and (fixnum? result) (fx>= result -1)
    453               (fx< result (%ral-count ls)))
    454 
     349              (fx< result (ral-count ls)))
    455350</enscript>
    456351
     
    459354<procedure>(ral-place-next ls k)</procedure>
    460355
    461 function (result)
    462 
    463 <enscript highlight=scheme>
    464 
    465 (_ ls k)
    466 requires (and (%ral? ls) (fixnum? k)
    467               (fx>= k 0) (fx< k (%ral-height ls)))
     356<enscript highlight=scheme>
     357function (result)
     358requires (and (ral? ls) (fixnum? k)
     359              (fx>= k 0) (fx< k (ral-height ls)))
    468360ensures  (and (fixnum? result) (fx>= result 0)
    469               (fx<= result (%ral-count ls)))
    470 
     361              (fx<= result (ral-count ls)))
    471362</enscript>
    472363
     
    475366<procedure>(ral-print ls)</procedure>
    476367
     368<enscript highlight=scheme>
    477369command ((old new (constantly #t)))
    478 
    479 <enscript highlight=scheme>
    480 
    481 (_ ls)
    482 requires (%ral? ls)
     370requires (ral? ls)
    483371ensures  new
    484 
    485372</enscript>
    486373
     
    489376<procedure>(ral-ref ls place)</procedure>
    490377
    491 function (result)
    492 
    493 <enscript highlight=scheme>
    494 
    495 (_ ls place)
    496 requires (and (%ral? ls) (fixnum? place)
    497               (fx>= place 0) (fx< place (%ral-count ls)))
    498 ensures  ((%ral-item? ls) result)
    499 
     378<enscript highlight=scheme>
     379function (result)
     380requires (and (ral? ls) (fixnum? place)
     381              (fx>= place 0) (fx< place (ral-count ls)))
     382ensures  ((ral-item? ls) result)
    500383</enscript>
    501384
     
    504387<procedure>(ral-remove! ls place)</procedure>
    505388
    506 command ((oldcount newcount (lambda (ls place) (%ral-count ls))))
    507 
    508 <enscript highlight=scheme>
    509 
    510 (_ ls place)
    511 requires (%ral? ls)
     389<enscript highlight=scheme>
     390command ((oldcount newcount (lambda (ls place) (ral-count ls))))
     391requires (ral? ls)
    512392ensures  (and (fx= newcount (fx- oldcount 1)))
    513 
    514393</enscript>
    515394
    516395==== ral-restructure
    517396
    518 <procedure>(or (ral-restructure ls width)
    519                (ral-restructure ls width max-height))</procedure>
    520 
    521 function (result)
    522 
    523 <enscript highlight=scheme>
    524 
    525 (_ ls width)
    526 requires (and (%ral? ls) (fixnum? width) (fx> width 1))
    527 ensures  (and (%ral? result)
    528               (fx= (%ral-count ls) (%ral-count result))
    529               (fx= (%ral-width result) width))
    530 
    531 (_ ls width max-height)
    532 requires (and (%ral? ls) (fixnum? width)
     397<procedure>(ral-restructure ls width)</procedure>
     398<procedure>(ral-restructure ls width max-height)</procedure>
     399
     400<enscript highlight=scheme>
     401function (result)
     402requires (and (ral? ls) (fixnum? width)
    533403              (fx> width 1) (fixnum? max-height) (fx> max-height 1))
    534 ensures  (and (%ral? result) (fx= (%ral-count ls) (%ral-count result))
    535               (fx= (%ral-width result) width)
    536               (fx= (%ral-max-height result) max-height))
    537 
     404         ; default (fx= max-height (ral-max-height ls))
     405ensures  (and (ral? result) (fx= (ral-count ls) (ral-count result))
     406              (fx= (ral-width result) width)
     407              (fx= (ral-max-height result) max-height))
    538408</enscript>
    539409
     
    542412<procedure>(ral-set! ls place item)</procedure>
    543413
    544 command ((old new (lambda (ls place item) (%ral-ref ls place))))
    545 
    546 <enscript highlight=scheme>
    547 
    548 (_ ls place item)
    549 requires (and (%ral? ls) ((%ral-item? ls) item)
     414<enscript highlight=scheme>
     415command ((old new (lambda (ls place item) (ral-ref ls place))))
     416requires (and (ral? ls) ((ral-item? ls) item)
    550417              (fixnum? place) (fx>= place 0)
    551               (fx< place (%ral-count ls)))
     418              (fx< place (ral-count ls)))
    552419ensures  (equal? new item)
    553 
    554420</enscript>
    555421
     
    558424<procedure>(ral-split ls place)</procedure>
    559425
     426<enscript highlight=scheme>
    560427function (head tail)
    561 
    562 <enscript highlight=scheme>
    563 
    564 (_ ls place)
    565 requires (and (%ral? ls) (fixnum? place)
    566               (fx>= place 0) (fx< place (%ral-count ls)))
    567 ensures  (and (%ral? head) (%ral? tail)
    568               (fx= (%ral-count head) place)
    569               (fx= (%ral-count tail) (fx- (%ral-count ls) place)))
    570 
     428requires (and (ral? ls) (fixnum? place)
     429              (fx>= place 0) (fx< place (ral-count ls)))
     430ensures  (and (ral? head) (ral? tail)
     431              (fx= (ral-count head) place)
     432              (fx= (ral-count tail) (fx- (ral-count ls) place)))
    571433</enscript>
    572434
     
    575437<procedure>(ral-start ls)</procedure>
    576438
    577 function (result)
    578 
    579 <enscript highlight=scheme>
    580 
    581 (_ ls)
    582 requires (%ral? ls)
    583 ensures  (%ral-node? result)
    584 
     439<enscript highlight=scheme>
     440function (result)
     441requires (ral? ls)
     442ensures  (ral-node? result)
    585443</enscript>
    586444
     
    589447<procedure>(ral-width ls)</procedure>
    590448
    591 function (result)
    592 
    593 <enscript highlight=scheme>
    594 
    595 (_ ls)
    596 requires (%ral? ls)
     449<enscript highlight=scheme>
     450function (result)
     451requires (ral? ls)
    597452ensures  (and (fixnum? result) (fx> result 1))
    598 
    599453</enscript>
    600454
     
    603457<procedure>(ral? xpr)</procedure>
    604458
    605 function (result)
    606 
    607 <enscript highlight=scheme>
    608 
    609 (_ xpr)
     459<enscript highlight=scheme>
     460function (result)
    610461requires #t
    611462ensures  (boolean? result)
    612 
    613463</enscript>
    614464
  • wiki/eggref/4/skiplists

    r31099 r31103  
    7070
    7171<enscript highlight=scheme>
    72 (dups x y)
    7372function (result)
    7473requires (and ((skiplist-item? sls) x) ((skiplist-item? sls) y))
     
    8382
    8483<enscript highlight=scheme>
    85 (skiplist width max-height item? order . orders)
    8684function (result)
    8785requires (and (fixnum? width)
    88               (fx> width 1)
    89               (fixnum? max-height)
     86              (fx> width 1) ; default (fx= width 2)
     87              (fixnum? max-height) ; default (fx= max-height 10)
    9088              (fx> max-height 1)
    9189              (procedure? item?)
     
    9694              " like order, last one might be dups")
    9795ensures  (skiplist? result)
    98 
    99 (skiplist max-height item? order . orders)
    100 "width defaults to 2"
    101 requires (and (fixnum? max-height)
    102               (fx> max-height 1)
    103               (procedure? item?)
    104               (item? item)
    105               (procedure? order)
    106               "(fixnum? (order item? item?))"
    107               ((list-of? procedure?) orders)
    108               " like order, last one might be dups")
    109 ensures  (skiplist? result)
    110 
    111 (skiplist item? order . orders)
    112 "width defaults to 2, max-height to 10"
    113 requires (and (procedure? item?)
    114               (item? item)
    115               (procedure? order)
    116               "(fixnum? (order item? item?))"
    117               ((list-of? procedure?) orders)
    118               " like order, last one might be dups")
    119 ensures  (skiplist? result)
    12096</enscript>
    12197
     
    126102
    127103<enscript highlight=scheme>
    128 (skiplist->list sls)
    129 function (result)
    130 requires (skiplist? sls)
    131 ensures  ((list-of? (skiplist-item? sls)) result)
    132 
    133 (skiplist->list sls level)
    134104requires (and (skiplist? sls)
    135105              (fixnum? level)
    136               (fx<= 0 level)
     106              (fx<= 0 level) ; default (fx= level 0)
    137107              (fx< level (skiplist-height sls)))
    138108ensures  ((list-of? (skiplist-item? sls)) result)
     
    144114
    145115<enscript highlight=scheme>
    146 (skiplist-clear! sls)
    147116command ((oldcount newcount skiplist-count) (oldheight newheight skiplist-height))
    148117requires (skiplist? sls)
     
    155124
    156125<enscript highlight=scheme>
    157 (skiplist-compare sls)
    158126function (result)
    159127requires (skiplist? sls)
     
    166134
    167135<enscript highlight=scheme>
    168 (skiplist-count sls)
    169136function (result)
    170137requires (skiplist? sls)
     
    177144
    178145<enscript highlight=scheme>
    179 (skiplist-dups? sls)
    180146function (result)
    181147requires (skiplist? sls)
     
    188154
    189155<enscript highlight=scheme>
    190 (skiplist-filter sls ok?)
    191156function (result)
    192157requires (and (skiplist? sls) (procedure? ok?) "(boolean? (ok? x))")
     
    199164
    200165<enscript highlight=scheme>
    201 (skiplist-for-each sls proc)
    202166command ((old new (constantly #t)))
    203167requires (and (skiplist? sls) (procedure? proc))
     
    210174
    211175<enscript highlight=scheme>
    212 (skiplist-found sls)
    213176function (result)
    214177requires (skiplist? sls)
     
    221184
    222185<enscript highlight=scheme>
    223 (skiplist-found? sls item)
    224186function (result)
    225187requires (and (skiplist? sls) ((skiplist-item? sls) item))
     
    232194
    233195<enscript highlight=scheme>
    234 (skiplist-height sls)
    235196function (result)
    236197requires (skiplist? sls)
     
    243204
    244205<enscript highlight=scheme>
    245 (skiplist-insert! sls item . items)
    246206command ((oldcount newcount (lambda (sls . items) (skiplist-count sls)))
    247207         (oldfound newfound (lambda (sls . items)
     
    258218
    259219<enscript highlight=scheme>
    260 (skiplist-item? sls)
    261220function (result)
    262221requires (skiplist? sls)
     
    272231
    273232<enscript highlight=scheme>
    274 (skiplist-map sls fn)
    275233function (result)
    276234requires (and (skiplist? sls)
     
    292250
    293251<enscript highlight=scheme>
    294 (skiplist-max sls)
    295252function (result)
    296253requires (skiplist? sls)
     
    303260
    304261<enscript highlight=scheme>
    305 (skiplist-max-height sls)
    306262function (result)
    307263requires (skiplist? sls)
     
    314270
    315271<enscript highlight=scheme>
    316 (skiplist-min sls)
    317272function (result)
    318273requires (skiplist? sls)
     
    325280
    326281<enscript highlight=scheme>
    327 (skiplist-null? sls)
    328282function (result)
    329283requires (skiplist? sls)
     
    336290
    337291<enscript highlight=scheme>
    338 (skiplist-orders sls)
    339292function (result)
    340293requires (skiplist? sls)
     
    347300
    348301<enscript highlight=scheme>
    349 (skiplist-remove! sls item . items)
    350302command ((oldcount newcount (lambda (sls . items)
    351303                              (skiplist-count sls))))
     
    360312
    361313<enscript highlight=scheme>
    362 (skiplist-reorder sls order . orders)
    363314function (result)
    364315requires (and (skiplist? sls)
     
    373324
    374325<enscript highlight=scheme>
    375 (skiplist-restructure sls width max-height)
    376326function (result)
    377327requires (and (skiplist? sls) (fixnum? width) (fx> width 1)
     
    385335
    386336<enscript highlight=scheme>
    387 (skiplist-search! sls item)
    388337command ((oldlevel newlevel (lambda (sls item)
    389338                              (skiplist-search-level sls)))
     
    404353
    405354<enscript highlight=scheme>
    406 (skiplist-search-level sls)
    407355function (result)
    408356requires (skiplist? sls)
     
    415363
    416364<enscript highlight=scheme>
    417 (skiplist-width sls)
    418365function (result)
    419366requires (skiplist? sls)
     
    426373
    427374<enscript highlight=scheme>
    428 (skiplist? xpr)
    429375function (result)
    430376requires #t
Note: See TracChangeset for help on using the changeset viewer.