QQ客服 官方微博 反馈留言

	On invariant checking
	Zhang Zhihai ; Kapur, Deepak
	2013
关键词	Assertion Floyd-Hoare logic invariant invariant generation SEMI-ALGEBRAIC SYSTEMS POLYNOMIAL INVARIANTS RANKING FUNCTIONS VERIFICATION GENERATION
英文摘要	Checking whether a given formula is an invariant at a given program location (especially, inside a loop) can be quite nontrivial even for simple loop programs, given that it is in general an undecidable property. This is especially the case if the given formula is not an inductive loop invariant, as most automated techniques can only check or generate inductive loop invariants. In this paper, conditions are identified on simple loops and formulas when this check can be performed automatically. A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop. As a byproduct of this analysis, a new kind of loop invariant inside the loop body, called inside-loop invariant, is proposed. Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification. The use of such invariants for program debugging is explored; it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow, accessing array/collection data structures outside the range, divide by zero, etc.; Mathematics, Interdisciplinary Applications; SCI(E); EI; 中国科学引文数据库(CSCD); 0; ARTICLE; 3; 470-482; 26
语种	英语
出处	EI ; SCI
出版者	journal of systems science complexity
内容类型	其他
源URL	[http://hdl.handle.net/20.500.11897/157474]
专题	数学科学学院
推荐引用方式 GB/T 7714	Zhang Zhihai,Kapur, Deepak. On invariant checking. 2013-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。