In the Cleanroom methodology, a verification function is
a shorthand notation for describing various program
entities. The author's preference is to use names for
these functions that contain a hyphen (“-”), so that it is clear that these are
not Python functions.
Our first verification function is lit-elt: an XML element that contains literate code.
#================================================================ # Verification functions #---------------------------------------------------------------- # lit-elt == an XML element whose GID is PROG_ELT, and which # has an attribute ROLE_ATTR whose value starts with # ROLE_PREFIX
Next is the lit-dest function. This
describes the destination file to which a literate
fragment is to be written.
#---------------------------------------------------------------- # lit-dest(elt) == the part of the ROLE_ATTR value after # ROLE_PREFIX in a lit-elt
The lit-content verification function
describes the text inside the literate fragment. Note
that literate code can contain XML tags: in some of the
author's source code, the DocBook link tag
is used so that the name of a called function or method
is a link to the definition of that function or method.
However, the source text should not include any tags.
#---------------------------------------------------------------- # lit-content(elt) == The text content of element (elt) and # any descendants #----------------------------------------------------------------