Dissertation > Excellent graduate degree dissertation topics show

Research on Loop Invariant Development Technology

Author: WanSongSong
Tutor: XueJinYun
School: Jiangxi Normal University
Course: Computer Software and Theory
Keywords: PAR method Loop invariant Loop variable Dijkstra weakest front predicate method
CLC: TP311.52
Type: Master's thesis
Year: 2008
Downloads: 68
Quote: 2
Read: Download Dissertation

Abstract

The high reliability of software is a hot issue in the software development today. Ensure that the logical structure of the algorithm program properly, the best way to formal derivation of the algorithm and prove. Loop invariant software formal methods occupies a very important position, it is the understanding of the basis of proof and derivation algorithm and key. Using formal methods to prove or derivation algorithm program can not avoid a problem is to give the correct loop invariant. However, loop invariants developed algorithm design has been the most challenging, the most creative, but also one of the most difficult problems. Since the formal methods appear, many experts is committed to loop invariant developers, the loop invariant development technology, such as predicate abstraction techniques, dynamic detection technology. These techniques can detect loop invariant, a relatively simple problem but can not deal with complex problems. In essence, the loop invariant characterizes the characteristics of the loop variable variation and recycling program, a recycling program cycle invariant is not easily able to get, especially for complex algorithm must cycle can be found based on the program algorithm is essentially fully understood. The existing loop invariant definition do not reflect the nature of loop invariant, the lack of theoretical guidance based on the existing loop invariant definition of the technology, the tentative detection loop invariant process and blindness loop invariant, but also because of their technical limitations, and therefore unable to conclude that the complex problems. Professor Xue Jinyun academic team analyzed a large number of the essential characteristics of the algorithm and its loop invariant relations [15] to [20] found that the deficiencies of the existing loop invariant definition proposed new loop invariant defined and based on the new definition of loop invariant over the development of technology, formed on the basis of a practical algorithm formal development method - PAR method and its development environment, the complex algorithm and software formal development played an important role. This article is a continuation of the study of the PAR method and its development environment,, Xue Jinyun auspices of the National Natural Science Foundation of commitment \important research content. The main work of this paper the existing loop invariant definition and the existing development technology to conduct in-depth research and development of technology PAR method loop invariant compare, point out the inadequacies of existing development technologies; based on both Professor Xue Jinyun loop invariants new definitions and new development technologies, explore, study and preliminary loop invariant automatic development system. Specific research results are as follows: depth study loop invariant definition; 2. Loop invariant standard development strategy and the newer several loop invariant development technology analysis and comparison, analysis of its difficult applicable; 3. detailed analysis of the PAR method loops the invariants new definitions and new development strategy, its proposed as the basis of a new model of the loop invariant development system, and the initial realization of the loop invariant automatically Development System; 4 Dijkstra weakest front predicate method developed loop invariant correctness proof.

Related Dissertations

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Software Engineering > Software Development
© 2012 www.DissertationTopic.Net Mobile