源代码转换方法和源代码转换程序

摘要

为了在软件的模型检查中，降低用模型检查器的输入语言描述检查代码的成本，存在将软件的源代码转换为检查代码的方法。因为用户只能选择单一的转换方式，所以存在抽象化水平的变更困难、用于追随源代码的设计变更的规则修正成本较高、用于用不同检查工具检查的规则修正成本较高等课题。本发明在将源代码转换为检查代码时，提供选择多个转换规则的单元，用户能够容易地变更抽象化的水平。此外，多个转换规则包括将源代码转换为中间形式的转换规则、在中间形式中进行抽象化的转换规则和从中间形式转换为检查代码的转换规则。