A form of semantic analysis/proof of a program in which symbols are used as input variables. The program is viewed as having an input state determined by the input data and the initial state of the program. For each line of the program a test is made to see if the state has changed. Each state change is recorded. A logical path through the program is converted into an ordered set of state changes. The final state for each path should be an output state or program termination. The program is proved correct if each sequence of inputs generates only the required output states.

The technique has been automated, but the size of program that can be handled is limited and manual assistance may be needed to handle loops correctly and efficiently. See also program correctness proof, static analysis.