In the inspection process, we rewrite the concurrent program by assigning each primitive statement a label; the transfer of control from statement to statement is made explicit. Auxiliary variables are used to record extra information for inspection without affecting the original intent of the program. The resulting program is a non-deterministic sequential program with the same behavioral effect as the original concurrent program. The rewritten program is then examined through checking the truth-value of the system invariant that fully captures program structure. A decreasing quantity of the program states is also used to show the clean completion of the program.
We use tabular expressions, program-function tables, to describe the function of the program. Each column in the table is inspected individually; the program is divided into small components to be conquered with ease. The correctness of the whole program is implied (evaluated) by the correctness of the columns examined through the inspection.