摘要
提出一种基于GCL语言生成程序测试用例的形式化方法.程序的语义为测试用例的生成提供了基本框架,而由Hoare等人提供的规则保证了用例的正确性.作者的这种方法可被认为是一种严格的,自动生成测试用例的方法.这种方法的优点在于:所获得的测试用例都是可行的,在测试用例生成过程中可以避免状态爆炸问题,而且该方法可以延拓到任何目标语言.据此开发了一个基于Haskell语言的原型工具来支持作者的方法.
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.
出处
《计算机学报》
EI
CSCD
北大核心
2014年第12期2492-2504,共13页
Chinese Journal of Computers
基金
国家自然科学基金(61170015,61210004)资助
