CAJ | 학술논문

在高度依赖软件的信息时代，程序的正确性验证问题需要深入研究。文中提出了基于抽象解释和数值熵的数值程序正确性分析方法。抽象解释理论为程序静态分析提供了一个通用框架，在编译时能够自动地推导程序的动态性质。数值信息熵能够反映变量的值范围，通过熵值的大小可以判断变量取值是否在规定范围内。通过一个C程序对该方法进行了验证，该数值程序分析方法可以做到对程序正确性等的验证，并且较单纯地抽象解释近似分析，正确性、可靠性更高。
재고도의뢰연건적신식시대，정서적정학성험증문제수요심입연구。문중제출료기우추상해석화수치적적수치정서정학성분석방법。추상해석이론위정서정태분석제공료일개통용광가，재편역시능구자동지추도정서적동태성질。수치신식적능구반영변량적치범위，통과적치적대소가이판단변량취치시부재규정범위내。통과일개C정서대해방법진행료험증，해수치정서분석방법가이주도대정서정학성등적험증，병차교단순지추상해석근사분석，정학성、가고성경고。
In the information age,software is highly dependent,thus the correctness of the program validation issues need to be further study. In the paper,introduce the value range analysis method based on abstract interpretation and value information entropy. The abstract interpretation as an important method of the static analysis,uses testing framework to deduce the program's dynamic property automati-cally. The value information entropy can reflect the range of a variable,through the entropy,can judge whether variable values within the prescribed scope. Through validating this method with C program,find the method can validate the correctness of the running program. Compared with the only abstract interpretation analysis,the method is higher in validity and reliability.