Abstract: A method of verifying data structure’s property is introduced, which is based on automated test generation. It combines the traditional model checking and the automated software test generation, and searches the state space orderly, while ensuring the soundness of generating states as well as the completeness of the coverage of state space. At the same time, the method of describing property is the program logic, which is familiar by programmers and easy to use.

Key words: automated test, property verification, program logic

摘要： 针对数据结构的性质，特别是链式数据结构，提出一种自动测试中的状态生成算法。结合传统的模型检测思想从自动测试生成的角度对程序的状态空间进行搜索，在有效地生成测试程序状态的同时保证了程序状态的完全覆盖。该方法采用程序员熟悉的程序逻辑的描述方法，更易于使用。

关键词: 自动测试, 性质验证, 程序逻辑

CLC Number: 

• TP301.6