Automated Test Case Generation from OTS/CafeOBJ Specifications by Specification Translation

摘要

A skeleton unit test code generation method has been proposed for OTS/CafeOBJ specifications. To obtain executable test codes, we need to instantiate those skeleton test codes. In this study, we propose a method to instantiate them with CafeOBJ rewrite specifications and the exhaustive search command. We compare rewrite specifications obtained by the existing specification translation methods from OTS/CafeOBJ specifications to rewrite specifications.