Verification of finite iterations over collections of variable data structures
- PDF / 143,585 Bytes
- 12 Pages / 595 x 842 pts (A4) Page_size
- 105 Downloads / 195 Views
VERIFICATION OF FINITE ITERATIONS OVER COLLECTIONS OF VARIABLE DATA STRUCTURES
UDC 519.172
V. A. Nepomniaschy
To extend the application domain of the symbolic verification method, finite iterations over collections of variable data structures are introduced and reduced to standard finite iterations. This reduction is extended to finite iterations including the break statement. The generalization of the symbolic method allows applying it to pointer program verification. Keywords: finite iterations, data structure, symbolic verification method, pointer program. INTRODUCTION The main approach to deductive verification of software is the axiomatic approach based on the Hoare method [1, 2]. It consists of the following stages: program annotation using preconditions, postconditions, and loop invariants and inference of correctness conditions with the help of rules of axiomatic semantics and their proof. In this approach, the synthesis of loop invariants is a difficult problem whose solution is far from satisfactory [3]. Attempts of extracting loop invariants from programs with the help of automatic means turned out to be fruitful only for special and sufficiently simple kinds of invariants [4]. In the functional approach to program verification, loops are annotated by functions expressing their actions [5, 6] but the synthesis of such functions also remains a difficult problem in most cases [5]. To overcome the mentioned difficulties of program verification, two approaches connected with constraints on postconditions and loop structures were used. Works on code certification are restricted to the verification of simple but important properties of programs within the framework of the axiomatic approach [7, 8]. However, the problem of synthesis of loop invariants imposes essential constraints on the practical application of the method proposed [8]. In [9], the so-called simple loops are selected whose behavior is similar to that of for-loops since they contain a unique control variable, namely, a loop variable whose change in a prescribed finite domain does not depend on the other variables modified by the loop body. Therefore, simple loops are finite, i.e., they always complete their execution. The general form of a finite iteration as an iteration over all the elements of an arbitrary data structure was proposed in [10] within the framework of the functional approach to program verification. The symbolic verification method that integrates the axiomatic and functional approaches is developed in [2, 11–13] for for-loops whose bodies consist of the statement of assignment to array elements. In [14, 15], this method is extended to finite iterations of general form. The method is based on the use of the replacement operation whose symbolical functional form represents the action of a for-loop and on a special technique of proving correctness conditions including the replacement operation. Along with the data structures specified in [10], the symbolic method makes it possible to use hierarchical data structures that are co
Data Loading...
