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 partial specificiation.

Last updated: 1996/03/09 22:31:50
URL: http://www.nmt.edu/~shipman/soft/clean/i-f.html