【摘 要】
：
在软件日益丰富的信息时代,程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释
【机 构】
：
安阳工学院计算机科学与信息工程学院,南京航空航天大学自动化学院
【基金项目】
：
国家自然科学基金（No.60674100）, 南京航空航天大学基本科研业务费专项科研项目（No.NS2010069）
论文部分内容阅读
在软件日益丰富的信息时代,程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析,提取不变量的抽象域区间;在抽象域区间上进行数值熵运算;运行程序获取数值变量的实际取值,计算数值熵;将抽象域区间数值熵和实际数值熵信息进行对比分析,准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围,而引入数值熵算法,在取值范围的基础上对程序静态分析的准确性进一步检验,同时也做到了对程序的正确性验证。通过C语言程序
其他文献
基于条件随机场模型在字粒度上识别并切分藏文人名,其优势是可以较好地利用藏文人名在文本中出现的基本特征和上下文特征来确定藏文人名在文本序列中的边界。根据藏文人名自
现今图像分割已然成为数字图像处理中必不可少的步骤之一,但是图像来源和目标形态的多样化使得至今还未有一种图像分割方法普遍适用于所有图像的分割。针对根系图像存在分支、根系交叉或重叠的现象,在现有算法的基础上,提出了一种基于形态学和距离变换相结合的分离方法。将形态学用于根系骨架交点膨胀,对根段图像利用改进的距离变换求其影响区,得到的影响区边界作为根系的分离线。实验证明和数据显示,该方法有效地解决了根系交