Next / Previous / Contents / TCC Help System / NM Tech homepage

4.2. Verification functions

The Cleanroom methodology relies on “verification functions” to describe notational shorthand. Here are all the verification functions used in this project, in alphabetical order.

All verification function names contain a hyphen, so you can distinguish them from program objects.

4.2.1. children-are-ordered

pyskip.py
#================================================================
# Verification functions
#----------------------------------------------------------------
# children-are-ordered ( x, y ) ==
#   if self.allowDups ->
#       cmp ( key-of ( x ), key-of ( y ) ) <= 0
#   else ->
#       cmp ( key-of ( x ), key-of ( y ) ) < 0
#--
# Similar to the keys-are-ordered predicate, but operates on
# child objects.

4.2.2. insertion-cut-list

pyskip.py
#----------------------------------------------------------------
# insertion-cut-list ( key ) ==
#   a list L of size self.__maxLevels, such that each element
#   L[i] equals insertion-point ( i, key )
#--
#   An ``insertion cut list'' is a list of the _SkipItem objects
#   that must be updated when a new elements is inserted.  Element
#   [i] of the cut list points to the element whose forward
#   pointer has to be repaired in the (i)th list.

4.2.3. insertion-point

pyskip.py
#----------------------------------------------------------------
# insertion-point ( level, key ) ==
#   the last element E in nth-list ( self.__heads, level ) such
#   that insertion-precedes ( E, key ) is true
#--
#   This describes the predecessor _SkipItem whose forward link
#   must be updated when a new item with key (key) is inserted.

4.2.4. insertion-point-after

pyskip.py
#----------------------------------------------------------------
# insertion-point-after ( level, key, searchItem ) ==
#   the last element E in nth-list(searchItem,level) such that
#   insertion-precedes(E, key) is true
#--
#   Just like insertion-point(), except that it starts at an
#   arbitrary _SkipItem instead of self.__heads.

4.2.5. insertion-precedes

pyskip.py
#----------------------------------------------------------------
# insertion-precedes ( skipItem, key ) ==
#   if skipItem is self.__terminator -> F
#   else if skipItem is self.__heads -> T
#   else ->
#     keys-are-ordered ( key-of ( skipItem's child ), key )
#--
#   This predicate is true when (skipItem) should be before
#   an item with key (key) in the level-0 list.

4.2.6. key-of

pyskip.py
#----------------------------------------------------------------
# key-of ( child ) ==
#   if  not self.keyFunction ->
#       child
#   else ->
#       self.keyFunction ( child )

4.2.7. keys-are-ordered

pyskip.py
#----------------------------------------------------------------
# keys-are-ordered ( x, y ) ==
#   if self.allowDups ->
#       cmp ( x, y ) <= 0
#   else ->
#       cmp ( x, y ) < 0
#--
#   This is the ordering relation used in the key domain.
#   -   If we don't allow duplicates, then each key must be
#       strictly less than its successor.
#   -   If we allow duplicates, then two successive keys can
#       be equal.

4.2.8. nth-list

pyskip.py
#----------------------------------------------------------------
# nth-list ( root, n ) ==
#   the linked list of _SkipItem objects rooted at (root) and
#   using _SkipItem.links[n] as the next-item method
#--
#   This define is used to describe positions in the linked list
#   of objects at one level of the structure.  In particular,
#       nth-list ( self.__heads, n )
#   describes the entire skip list at level (n).

4.2.9. search-cut-list

pyskip.py
#----------------------------------------------------------------
# search-cut-list ( key ) ==
#   a list L of size self.__maxLevels such that
#   L[i] := search-point ( i, key )
#--
#   Like insert-cut-list(), but used for .delete() and .find()
#   operations.

4.2.10. search-point

pyskip.py
#----------------------------------------------------------------
# search-point ( level, key ) ==
#   the last _SkipItem E in nth-list(self.__heads, level) such that
#   search-precedes(E, key) is true
#--
#   The predecessor whose forward link must be updated when
#   the item with key (key) is deleted.  Also used in
#   .find().

4.2.11. search-point-after

pyskip.py
#----------------------------------------------------------------
# search-point-after ( level, key, searchItem ) ==
#   the last element E in nth-list(searchItem, level) such that
#   search-precedes(E, key) is true
#--
#   Like search-point except that the search starts at some
#   given item rather than at self.__heads.

4.2.12. search-precedes

pyskip.py
#----------------------------------------------------------------
# search-precedes ( skipItem, key ) ==
#   if skip-compare ( skipitem, key ) < 0  ->  true
#   else -> false
#--
#   A predicate, true when the child in skipItem is before the
#   key (key).

4.2.13. skip-compare

pyskip.py
#----------------------------------------------------------------
# skip-compare ( skipItem, key ) ==
#   if skipItem is self.__terminator -> 1
#   else -> cmp ( key-of ( skipItem's child ), key )
#--
#   Like cmp(), but we want to avoid trying to extract a key
#   from self.__terminator, because it doesn't have one.  If
#   skipItem is the terminator, we return 1 because the terminator
#   goes after all other elements.
#----------------------------------------------------------------