首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   6篇
  国内免费   1篇
  完全免费   6篇
  自动化技术   13篇
  2017年   1篇
  2016年   1篇
  2015年   1篇
  2014年   1篇
  2013年   1篇
  2012年   2篇
  2010年   1篇
  2006年   1篇
  2005年   2篇
  1999年   1篇
  1997年   1篇
排序方式: 共有13条查询结果,搜索用时 171 毫秒
1.
区间上非线性程序的终止性判定   总被引:3,自引:1,他引:2       下载免费PDF全文
姚勇 《软件学报》2010,21(12):3116-3123
分析了如下类型程序的终止性:While x∈Ω do {x:=f(x)} end.其中,x是程序变量,Ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界,则上述结果是充要条件.仅仅在区间边界上有不动点的情况下,对函数略加限制,也建立了相应结果.特别地,对逐段多项式连续函数程序的终止性给出了完备判定算法.  相似文献
2.
Termination of Nested and Mutually Recursive Algorithms   总被引:1,自引:0,他引:1  
This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion.We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthys f_91 function).  相似文献
3.
We propose novel algebraic proof techniques for rewrite systems. Church–Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation.  相似文献
4.
主动规则集的可终止性是主动数据库规则集的三大重要特征之一.主动规则集可否保证终止将直接影响到系统的应用.由于主动规则间存在依赖关系,通过对依赖关系的分析,给出了规则的触发传递闭包、依赖传递闭包等概念.以此为基础,提出了用规则触发-依赖图(T—DG)方法来分析主动规则集的终止性.特别讨论了判定含环的触发图(TG)对应的主动规则集是否保证终止的方法,给出了相应的判定算法、算法证明及分析.  相似文献
5.
This paper describes the implementation of the Refined Triggering Graph (RTG) method for active rule termination analysis and provides an evaluation of the approach based on the application of the method to a sample active application. The RTG method has been defined in the context of an active-deductive, object-oriented database language known as CDOL (Comprehensive, Declarative, Object Language). The RTG method studies the contents of rule pairs and rule cycles in a triggering graph and tests for: (1) the successful unification of one rule's action with another rule's triggering event, and (2) the satisfiability of active rule conditions, asking whether it is possible for the condition of a triggered rule to evaluate to true in the context of the triggering rule's condition. If the analysis can provably demonstrate that one rule cannot trigger another rule, the directed vector connecting the two rules in a basic triggering graph can be removed, thus refining the triggering graph. An important aspect in the implementation of the method is the development of a satisfiability algorithm for CDOL conditions. This paper presents the tool that was developed based on the RTG method, describing how techniques from constraint logic programming are integrated with other techniques for testing the satisfiability of rule triggering conditions. The effectiveness of the approach within the context of a sample application is also addressed.  相似文献
6.
Numerical computations form an essential part of almost any real-world program. Traditional approaches to termination of logic programs are restricted to domains isomorphic to (ℕ,>); more recent works study termination of integer computations where the lack of well-foundedness of the integers has to be taken into account. Termination of computations involving floating-point numbers can be counterintuitive because of rounding errors and implementation conventions. We present a novel technique that allows us to prove termination of such computations. Our approach extends the previous work on termination of integer computations. Alexander Serebrenik: This research has been carried out during the first author's stay at the Department of Computer Science, K.U. Leuven, Belgium and STIX, école Polytechnique, France.  相似文献
7.
单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少。利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法。同时,对几类特殊循环的终止性进行了分析,得出了相应的结论。  相似文献
8.
为满足用户对网络服务的个性化、定制化和主动化需求,主动规则成为解决这些问题的关键技术.研究了在网络环境下基于规则的复杂应用中,大量规则集同时触发所带来的规则终止性问题,提出的分析方法确保主动规则能够有效运行,以提供更加灵活的主动服务.讨论了以静态分析方法为主的主动规则终止性分析相关工作,随后给出问题描述和相关形式化定义.分析了基于关联图的终止性分析方法的保守性,引入触发路径和有限触发环概念,提出了基于触发路径的两种终止情形分析方法,提高了规则集终止性分析的准确性,采用两阶段分析算法保证了分析效率.与相关分析方法的实验比较说明,文中方法能够更准确高效地检测主动规则集的终止性,并适应基于主动规则的其它应用.  相似文献
9.
李轶  吴文渊  冯勇 《软件学报》2014,25(6):1133-1142
对有界闭域上的线性赋值循环程序终止性问题进行研究.利用Jordan 标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题.证明了当线性迭代映射满足一定条件时,该类循环程序不可终止的充分必要条件是:迭代映射在有界闭域上有不动点或周期轨.  相似文献
10.
李轶  冯勇 《软件学报》2016,27(3):517-526
运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法. 该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号