A skip list container class in Python

Now we turn to the actual SkipList class. First, the external interface with intended functions:

# - - - - -   c l a s s   S k i p L i s t   - - - - -

class SkipList:
    """Container class for ordered sets.

      Exports:
        SkipList ( keyFun=None, cmpFun=None, allowDups=0,
                   count=1000000 ):
          [ (keyFun is a function that returns the key for a
             given child object) and
            (cmpFun is a function that compares two keys, using
             the usual Python convention for the cmp() function,
             or None use the built-in cmp() function) and
            (allowDups is 0 to refuse duplicate entries or 1 to
             allow them) and
            (count is a worst-case maximum element count) ->
              return a new, empty SkipList instance with those
              properties ]
        .insert(c):
          [ c is a child object ->
              if ((self contains an object whose key equals the key
                   of e) and (self.allowDups is false)) ->
                raise KeyError
              else ->
                self  :=  self with e added as a new child object ]
        .delete(k):
          [ k is in the key domain ->
              if self contains any child objects with keys equal to k ->
                self  :=  self with the first-inserted such child object
                          deleted
                return that child object
              else ->
                return None ]
        .match(k):
          [ k is in the key domain ->
              if self contains any child objects whose keys equal k ->
                return the first such child object
              else -> raise KeyError ]
        .find(k):
          [ k is in the key domain ->
              if self contains any child objects whose keys are >= k ->
                return an iterator that will iterate over all
                child objects whose keys are >= k, in order ]
        .__len__(self):
          [ return the number of child objects in self ]
        .__iter__(self):
          [ return an iterator that will iterate over all the
            child objects in self in order ]
        .__contains__(self, k):
          [ if self contains any child objects whose keys equal k ->
              return 1
            else -> return 0 ]
        .__delitem__(self, k):      [ same as self.delete(k) ]
        .__getitem__(self, k):      [ same as self.match(k) ]
        .nSearches:  [INVARIANT: Number of searches performed ]
        .nCompares:  [INVARIANT: Number of child pairs compared ]
    """

Next, we declare a manifest constant for the Pugh's p:

#--
# Manifest constants
#--
    NEW_LEVEL_PROBABILITY   = 0.25  # The `p' of Pugh's article

Next, we need to declare the class's internal state and invariants.

#================================================================
# State and invariants
#----------------------------------------------------------------
# .keyFun:       [ as passed to constructor, read-only ]
# .cmpFun:       [ as passed to constructor, read-only ]
# .allowDups:    [ as passed to constructor, read-only ]
# .__maxLevels:
#   [ 1 + ceiling ( log (base 4) of count argument to constructor ) ]
# .__nLevels:
#   [ number of levels currently in use ]
#   INVARIANT: 1 <= self.__nLevels <= self.__maxLevels ]
# .__heads:
#   [ list of head pointers to each level ]
#   INVARIANT: self.__heads.links[0] is the head of a linked list
#   of _SkipItem objects, terminated by a link to self.__terminator,
#   and whose members contain all the child objects currently in
#   self, such that for any two adjacent objects (Xi, Xj),
#   children-are-ordered ( Xi, Xj ) is true.
#
#   INVARIANT: For i in [0,self.__maxLevels), the list rooted in
#   heads.links[i] is a linked list of _SkipItem objects,
#   terminated by a link to self.terminator, and containing
#   a subset of the linked list in heads.links[i-1] in the same order.
# .__terminator:    [ terminator for all linked lists ]
#   INVARIANT: self.terminator is a _SkipItem object with
#   self.__maxLevels forward links all pointing to itself
# .__nItems:        [ INVARIANT: number of child items in self ]
#--