The method of test case generation based on GCL language

A formal method is presented to generate test cases for programs written in Guarded-Command-Language (GCL). The laws provided by Hoare et al. guarantee the correctness of the test cases. Semantics of the language provides the framework for the test case generation. Our method may be considered as a rigorous and automatic approach to the test case generation. From this method, we can get at least the following benefits: all the test cases are feasible, the state explosion problem can be avoided in the test case generation process, and this method can be extended to any target languages. A prototype tool written in Haskell has been built to support our method.