函数依赖似然不变量发现方法研究  

Research on Discovering Function-Dependent Likely Invariant

作　　者：刘杰[1] 

机构地区：[1]南华大学计算机与科学技术学院,衡阳421001

出　　处：《现代计算机》2008年第5期33-36,共4页Modern Computer

基　　金：湖南省自然科学基金项目(No.05JJ30117)

摘　　要：不变量是用于描述程序运行时不变性质的一些重要的逻辑断言。大型程序似然不变量发现的方法是通过对程序运行时的轨迹进行分析来获取的。以数据库理论为基础,将不变量形式分为函数依赖不变量和非函数依赖不变量,提出了函数依赖不变量动态发现方法,解决了目前试探法具有盲目性和效率不高的问题。Invariants are important logic assertions which describes the properties that are true when running the program . The technique of likely invariants discovery in large program is to infer them from captured variable traces. Based on the theory of database, classifies invariants into function-dependent and function-independent invariants and proposes methods for dynamically discovering function-independent ones. It helps to resolve such problems as blindness and inefficiency in detecting invariants.

关 键 词：程序不变量 函数依赖 不变量动态发现 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]