Next / Previous / Contents / Shipman's homepage

8. Specification functions

This block of comments defines some notational shorthand used in the Cleanroom verification process.
# - - - - -   S p e c i f i c a t i o n   f u n c t i o n s

8.1. ref-key

This notational shorthand refers to the composite key that is used to order the references to a given keyword. The keyword is the primary key, but the suffix, and then the prefix, are used as secondary and tertiary keys. We add vertical bars between the pieces so that, for example, word "abc" and suffix "xyz" will be treated differently than word "abcxy" and suffix "z".
# - - -   r e f - k e y

# The key value used to order one reference to a keyword, where
# ref is an instance of the KwicRef class.
# ref-key(ref) == ref.word + "|" + ref.suffix + "|" + ref.prefix