© 1984 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Proof of Correctness of Decision Table Programs
Department of Information and Computer Sciences, University of Hawaii at Manoa, Honolulu, USA
Proof methods adequate for computer programs expressed in a wide range of languages are well developed. One program construct, however, has been neglectednamely, 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.
Received May 1983.
* Permanent address: Department of Information and Computer Sciences, University of Hawaii at Manoa, Honolulu, Hawaii 96822, USA.
Oxford University Computing Laboratory, Programming Research Group, Oxford OX1 3QD, UK