Next / Previous / Contents / Shipman's homepage

4.5. Verification functions

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.

litlxml
#================================================================
# 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.

litlxml
#----------------------------------------------------------------
# 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.

litlxml
#----------------------------------------------------------------
# lit-content(elt)  ==  The text content of element (elt) and
#    any descendants
#----------------------------------------------------------------