/ Shipman's Home Sweet Homepage
/ Site map
Writing Cleanroom intended functions
If we are to be able to verify the implementation of a module,
we must have a semantic notation that clearly specifies what that module
does. In the Cleanroom methodology, a routine's semantics are specified
by writing them as an intended function, or I/F for short.
- First let's look at
simple intended functions, for
modules that always perform the same operation.
- Once you understand simple intended functions, we will
learn how to combine them with conditionals to make
compound intended functions.
- Finally, in many cases it is not possible (or even necessary)
to specify what a procedure does in every case; see
Next: Permissible Cleanroom control structures
See also: Overview of the Cleanroom software methodology
John W. Shipman,
Last updated: 1996/03/09 22:31:50