一种C语言核心语句转换到一阶公式的方法

摘要

一种C语言核心语句转换到一阶公式的方法：(1)使用现有的编译技术统计输入的C语言程序中使用的不同变量，将用于有序状态变元集合的生成；(2)逐条输入语句，判断语句的类型，并根据判断结果调用相应的转换模块，包括赋值语句转换模块，条件语句转换模块，while语句转换模块，过程调用语句转换模块，各模块根据相应语句的语义解释进行转换，并返回生成的新公式NewFormula；(3)处理完该条语句后，使用顺序语句规则，把得到的新公式NewFormula同当前公式CurFormula合并，结果存储在CurFormula中，然后转到步骤2。本发明根据程序语义的一种解释方法，把C语言核心语句转换成一阶公式，为基于R演算的软件测试机械化提供了前期的技术支持。

主权项

一种C语言核心语句转换到一阶公式的方法，其特征在于步骤如下：(1)输入C语言程序，该程序仅由C语言核心语句构成，即只涉及赋值语句、条件语句、while语句和过程调用语句，各语句之间的连接使用顺序语句，同时判断条件只是单个条件，并且只跟零作比较；此外程序中的变元和常元都是定义在自然数集合上，并且涉及的运算只包括加、减和乘；使用现有的编译技术统计程序中使用的不同变元的个数k，给这些变元按字典排序法排序，记为v＝{v1，…，vk}，所述v＝{v1，…，vk}为按字典排序法排序的程序中所使用的不同变元的有序集合；(2)全局变量count用来标记当前已经使用过的有序状态变元集合的个数，初始值为0；全局变量while_count用来标记当前已经处理过的while语句个数，初始值为0；变量CurFormula用来存储当前的一阶公式，初始值为空；变量NewFormula用来存储返回的新公式，初始值为空；(3)输入程序的第一条语句；(4)判断当前输入的语句的类型，根据判断结果调用相应的转换模块，包括赋值语句转换模块，条件语句转换模块，while语句转换模块，过程调用语句转换模块，各模块根据相应语句的语义解释进行转换，并返回生成的新公式NewFormula；(5)处理完当前输入的语句后，使用顺序语句规则，把当前返回的新公式NewFormula与当前的一阶公式CurFormula合并，结果存储在CurFormula中。判断程序是否结束，若没有，则输入程序的下一条语句，然后转到步骤(4)，否则，返回当前的CurFormula。