(index ("dups" 0) ("skiplist" 245) ("skiplist" 245) ("skiplist" 245) ("skiplist->list" 965) ("skiplist->list" 965) ("skiplist-clear!" 1330) ("skiplist-compare" 1580) ("skiplist-count" 1779) ("skiplist-dups?" 1960) ("skiplist-filter" 2120) ("skiplist-for-each" 2333) ("skiplist-found" 2532) ("skiplist-found?" 2715) ("skiplist-height" 2916) ("skiplist-insert!" 3098) ("skiplist-item?" 3611) ("skiplist-map" 3773) ("skiplist-map" 3773) ("skiplist-map" 3773) ("skiplist-map" 3773) ("skiplist-max" 4456) ("skiplist-max-height" 4635) ("skiplist-min" 4825) ("skiplist-null?" 5004) ("skiplist-orders" 5164) ("skiplist-remove!" 5339) ("skiplist-reorder" 5683) ("skiplist-restructure" 5974) ("skiplist-search!" 6255) ("skiplist-search-level" 6882) ("skiplist-width" 7112) ("skiplist?" 7292))
(def (sig (procedure "(dups x y)" (id dups))) (p "trivial numerical comparison operator to allow for duplicates") (highlight scheme "function (result)\nrequires (and ((skiplist-item? sls) x) ((skiplist-item? sls) y))\nensures  (fx= result 0)"))
(def (sig (procedure "(skiplist width max-height item? order . orders)" (id skiplist)) (procedure "(skiplist max-height item? order . orders)" (id skiplist)) (procedure "(skiplist item? order . orders))" (id skiplist))) (highlight scheme "function (result)\nrequires (and (fixnum? width)\n              (fx> width 1) ; default (fx= width 2)\n              (fixnum? max-height) ; default (fx= max-height 10)\n              (fx> max-height 1)\n              (procedure? item?)\n              (item? item)\n              (procedure? order)\n              \"(fixnum? (order item? item?))\"\n              ((list-of? procedure?) orders)\n              \" like order, last one might be dups\")\nensures  (skiplist? result)"))
(def (sig (procedure "(skiplist->list sls)" (id skiplist->list)) (procedure "(skiplist->list sls level)" (id skiplist->list))) (highlight scheme "requires (and (skiplist? sls)\n              (fixnum? level)\n              (fx<= 0 level) ; default (fx= level 0)\n              (fx< level (skiplist-height sls)))\nensures  ((list-of? (skiplist-item? sls)) result)"))
(def (sig (procedure "(skiplist-clear! sls)" (id skiplist-clear!))) (highlight scheme "command ((oldcount newcount skiplist-count) (oldheight newheight skiplist-height))\nrequires (skiplist? sls)\nensures  (and (fx= 0 newcount) (fx= 1 newheight))"))
(def (sig (procedure "(skiplist-compare sls)" (id skiplist-compare))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (and (procedure? result) \"(fixnum? (result x y))\")"))
(def (sig (procedure "(skiplist-count sls)" (id skiplist-count))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (and (fixnum? result) (fx>= result 0))"))
(def (sig (procedure "(skiplist-dups? sls)" (id skiplist-dups?))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (boolean? result)"))
(def (sig (procedure "(skiplist-filter sls ok?)" (id skiplist-filter))) (highlight scheme "function (result)\nrequires (and (skiplist? sls) (procedure? ok?) \"(boolean? (ok? x))\")\nensures  (skiplist? result)"))
(def (sig (procedure "(skiplist-for-each sls proc)" (id skiplist-for-each))) (highlight scheme "command ((old new (constantly #t)))\nrequires (and (skiplist? sls) (procedure? proc))\nensures  new"))
(def (sig (procedure "(skiplist-found sls)" (id skiplist-found))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  ((list-of? (skiplist-item? sls)) result)"))
(def (sig (procedure "(skiplist-found? sls item)" (id skiplist-found?))) (highlight scheme "function (result)\nrequires (and (skiplist? sls) ((skiplist-item? sls) item))\nensures  (boolean? result)"))
(def (sig (procedure "(skiplist-height sls)" (id skiplist-height))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (and (fixnum? result) (fx> result 0))"))
(def (sig (procedure "(skiplist-insert! sls item . items)" (id skiplist-insert!))) (highlight scheme "command ((oldcount newcount (lambda (sls . items) (skiplist-count sls)))\n         (oldfound newfound (lambda (sls . items)\n                              (skiplist-search! sls (car items))\n                              (skiplist-found sls))))\nrequires (and (skiplist? sls)\n              ((list-of? (skiplist-item? sls)) (cons item items)))\nensures  (and (fx>= newcount oldcount) (member item newfound))"))
(def (sig (procedure "(skiplist-item? sls)" (id skiplist-item?))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (procedure? result)"))
(def (sig (procedure "(skiplist-map sls fn)" (id skiplist-map)) (procedure "(skiplist-map sls fn order . orders)" (id skiplist-map)) (procedure "(skiplist-map sls fn width)" (id skiplist-map)) (procedure "(skiplist-map sls fn width order . orders)" (id skiplist-map))) (highlight scheme "function (result)\nrequires (and (skiplist? sls)\n              (procedure? fn)\n              \"((skiplist-item? sls) (fn x))\")\nensures  (skiplist? result)\n\n(skiplist-map sls fn item? order . orders)\nrequires (and (skiplist? sls)\n              (procedure? fn)\n              (procedure? item?)\n              (((list-of? procedure?) (cons order orders))))\nensures  (skiplist? result)"))
(def (sig (procedure "(skiplist-max sls)" (id skiplist-max))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  ((list-of? (skiplist-item? sls)) result)"))
(def (sig (procedure "(skiplist-max-height sls)" (id skiplist-max-height))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (and (fixnum? result) (fx> result 1))"))
(def (sig (procedure "(skiplist-min sls)" (id skiplist-min))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  ((list-of? (skiplist-item? sls)) result)"))
(def (sig (procedure "(skiplist-null? sls)" (id skiplist-null?))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (boolean? result)"))
(def (sig (procedure "(skiplist-orders sls)" (id skiplist-orders))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  ((list-of? procedure?) result)"))
(def (sig (procedure "(skiplist-remove! sls item . items)" (id skiplist-remove!))) (highlight scheme "command ((oldcount newcount (lambda (sls . items)\n                              (skiplist-count sls))))\nrequires (and (skiplist? sls)\n              ((list-of? (skiplist-item? sls)) (cons item items)))\nensures  (fx<= newcount oldcount)"))
(def (sig (procedure "(skiplist-reorder sls order . orders)" (id skiplist-reorder))) (highlight scheme "function (result)\nrequires (and (skiplist? sls)\n              ((list-of? procedure?) (cons order orders))\n              \"each (fixnum? (order x y))\")\nensures  (skiplist? result)"))
(def (sig (procedure "(skiplist-restructure sls width max-height)" (id skiplist-restructure))) (highlight scheme "function (result)\nrequires (and (skiplist? sls) (fixnum? width) (fx> width 1)\n              (fixnum? max-height) (fx> max-height 1))\nensures  (skiplist? result)"))
(def (sig (procedure "(skiplist-search! sls item)" (id skiplist-search!))) (highlight scheme "command ((oldlevel newlevel (lambda (sls item)\n                              (skiplist-search-level sls)))\n         (oldfound newfound (lambda (sls item) (skiplist-found sls))))\nrequires (and (skiplist? sls)\n              ((skiplist-item? sls) item))\nensures  (and (fx>= newlevel 0)\n              (fx< newlevel (skiplist-height sls))\n              ((list-of? (skiplist-item? sls)) newfound)\n              ((list-of? zero?)\n               (map (lambda (x) ((skiplist-compare sls) item x))\n                    newfound)))"))
(def (sig (procedure "(skiplist-search-level sls)" (id skiplist-search-level))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (and (fixnum? result) (fx>= result 0) (fx< result (skiplist-height sls)))"))
(def (sig (procedure "(skiplist-width sls)" (id skiplist-width))) (highlight scheme "function (result)\nrequires (skiplist? sls)\nensures  (and (fixnum? result) (fx> result 1))"))
(def (sig (procedure "(skiplist? xpr)" (id skiplist?))) (highlight scheme "function (result)\nrequires #t\nensures  (boolean? result)"))
