Abstract
Proof methods adequate for computer programs expressed in a wide range of languages are well developed. One program construct, however, has been neglected—namely, that of decision tables. It is shown here how decision table programs can be proved correct. The use of their level structure and the treatment of ‘impossible’ rules are of special significance. The method is illustrated by a proof of a bubble sort algorithm.

This publication has 0 references indexed in Scilit: