One important technique from the Cleanroom methodology is the use of trace tables to assist the verification panel in the inspection of the code.
For some simpler modules, there is a single sequence of trace tables that traces the state changes through that module. For each numbered prime (primary program refinement) of the module, we display first the intended function for that prime, followed by a table showing the values of all state items whose state has changed. The final set of state changes should match the overall intended function of the module.
In general, however, there are multiple trace table sequences for different cases of the logic. In that case, the trace table exposition for that module starts out with a list of all the cases. For each case, there is a trace table sequence showing the state changes in that case.