【作者】 刘杰；

【导师】 阳小华；

【作者基本信息】 南华大学 ， 计算机应用技术， 2008， 硕士

【摘要】 随着计算机技术的发展,软件在各个行业得到广泛的应用,人们对软件的质量和安全也得到更为广泛的关注。对如何提高软件质量的问题人们已经从软件开发方法、软件开发过程管理、软件开发工具等多个方面加以研究,取得了一定的成绩。基于合约的软件开发是其中十分重要且得到广泛应用的一种技术。软件合约是指软件中必须遵守的规则。开发者和执行者通过遵守这些合约来保证软件的质量。从不同的层面合约可分为语法合约、数据合约、行为合约和服务合约。程序不变量是数据合约的一种形式。程序不变量对于程序演进与重构、程序测试与排错、辅助定理证明、构件升级替换都有重要作用。由于大多数软件开发时都没有书写形式化文档,程序不变量在程序中很少被清楚地表示出来。如何从程序中发现这些隐含的没有被程序员写出来的程序不变量成为实现高层次行为合约、提高程序质量的关键。本文重点研究如何使用动态检测技术发现程序中函数型似然不变量。论文首先介绍了不变量动态检测技术及其主要的两个实现工具:Daikon和DIDUCE,并分析了它们在编配工具和不变量检测方法上存在的不足。然后运用面向对象的软件开发方法,设计并实现了一个新的基于关系数据库的编配工具。新的编配工具具有易用、灵活等特点。结合关系数据理论,针对函数型不变量提出了一个启发式不变量检测方法。该方法通过函数推导技术首先确定待检变量中是否存在函数依赖关系,然后再进行函数解析式推导,解决了传统似然不变量检测方法中存在的盲目性问题。并对新方法和传统方法进行了对比实验分析,实验结果表明新方法的可靠性与检测效率明显优于传统方法。更多还原

【Abstract】 Along with the devolepment of computer science, softwares are widely applied in kinds of business. The quality and security of software cause more serious attention than before. In order to guarantee the quality of software, people has researched various respects such as software developing methods, management of software development process and software developing tools and made a good progress. Design by contract is a very important widely applied method of building quality software.Contracts are formal specifications that must be followed when developping software, which can be classified into four levels,grammer contract,data contract,behavior contract and service contract.Software supplier and client ensure qualify by organizing their collaboration on the basis of those contracts. Invariant is the basic fabric of data contract, which is valueable for program revolution, verification, rebuilding, testing, debugging and updating. However most software are lack of specified documents, invariants are not explicitly stated.To discovery the implicit invariants from program is essential for implementing behaviour constract and improving the program reliability.This paper focus on dynamic detecting techniques in discovering function likely invariants.the concepts and traditional approaches (daikon and Diduce) are dicussed first. After analysing the disvantages of the two techniques,a new instrument tool base on database is introduced,which is disigned and implemented byobject-oriented method.A heuristic detecting method with a high degree of flexibility,ease of use assosiated with database is proposed . In this new method, whether the expected variables are dependent with function is checked before inferential reasoning function parsing formula so that it resolves the problem of blindly detecting in tradtional method. Finally, experiments have been done to compare tradtional method and the new one which demonstrate that the latter is obviously better in detecting realibility and effeciency.更多还原