摘要
本文主要讨论基于合约的似然程序不变量的内涵,以及通过程序断言动态生成技术来发现程序不变量的意义。在此主要描述基于合约的似然程序不变量发现的基本理论模型以及该模型与动态不变量检测工具Daikon实体模型的比较,进一步论述程序断言动态生成技术。通过精确的程序断言动态生成,可以分析程序各变量之间的关联属性,以完成不变量的检测。从而有助于设计高质量的程序架构以及规范化的程序代码.
This paper mainly discusses the connotation of the likely program invariants which base on the program contract and the meaning of discovering program invariants by the technology of dynamically making program assertion. In order to discourse the technology of the dynamically making the program assertion, this paper introduces the base theory model of the discovering likely program invariants based on the contract and the comparison between the entity model of Daikon which is a tool of dynamically discovering the invariants of program and the theory model. Using the accurate program assertion, the programmer can analyze the associate-attributes among the variants of program and achieve the detecting of the invariants. So designing the standard program frames and program codes of high quality can benefit from the program assertion.
出处
《微计算机信息》
北大核心
2006年第10X期233-235,300,共4页
Control & Automation
基金
湖南省自然科学基金课题资助
项目名称:程序断言动态生成技术
项目编号:05JJ30117
关键词
程序不变量
关联属性
程序断言
合约
program invariant,associate-attribute,Program assertion,contract
