Abstract
A method of verifying a definite iteration over hierarchical data structures is proposed. The method is based on a replacement operation which expresses the definite iteration effect in a symbolic form and belongs to a specification language. The method includes a proof rule for the iteration without invariants and inductive proof principles for proving verification conditions which contain the replacement operation. As a case study, a parallel replacement operation for arrays is considered in order to simplify the proof of verification conditions. Examples which illustrate the application of the method are considered.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Basu, S.K., Misra, J.: Proving loop programs. IEEE Trans. on Software Engineering 1(1), 76–86 (1975)
Basu, S.K., Misra, J.: Some classes of naturally provable programs. In: Proc. 2nd Int. Conf. on Software Engineering, pp. 400–406. IEEE Press, Los Alamitos (1976)
Chandy, K.M., Misra, J.: Parallel Program Design. Addison-Wesley, Reading (1988)
Dunlop, D.D., Basili, V.R.: Generalizing specifications for uniformly implemented loops. ACM Trans. on Programming Languages and Systems 7(1), 137–158 (1985)
Fradet, P., Gaugne, R., Metayer, D.L.: Static detection of pointer errors: an axiomatisation and a checking algorithm. Lecture Notes in Computer Sci. vol. 1058, 125–140 (1996)
Gries, D., Gehani, N.: Some ideas on data types in high-level languages. Communications of the ACM 20(6), 414–420 (1977)
Hoare, C.A.R.: An axiomatic basis of computer programming. Communications of the ACM 12(10), 576–580 (1969)
Hoare, C.A.R.: A note on the for statement. BIT 12(3), 334–341 (1972)
Linger, R.C., Mills, H.D., Witt, B.I.: Structured Programming: Theory And Practice, Addison-Wesley, Reading (1979)
Mills, H.D.: Structured programming: retrospect and prospect. IEEE Software 3(6), 58–67 (1986)
Nepomniaschy, V.A.: Proving correctness of linear algebra programs. Programming 4, 63–72 (1982) (in Russian)
Nepomniashy, V.A.: Loop invariant elimination in program verification. Programming 3, 3–13 (1985) (in Russian)
Nepomniaschy, V.A.: On problem-oriented program verification. Programming 1, 3–13 (1986) (in Russian)
Nepomniaschy, V.A.: Verification of definite iteration over data structures without invariants. In: Proc. 12th Intern. Symp. on Computer and Information Sci., Antalya, Turkey, pp. 608–614 (1997)
Reynolds, J.C.: Reasoning about arrays. Comm. of the ACM 22(5), 290–299 (1979)
Stavely, A.M.: Verifying definite iteration over data structures. IEEE Trans. on Software Engineering 21(6), 506–514 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nepomniaschy, V.A. (1999). Verification of Definite Iteration over Hierarchical Data Structures. In: Finance, JP. (eds) Fundamental Approaches to Software Engineering. FASE 1999. Lecture Notes in Computer Science, vol 1577. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49020-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-49020-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65718-7
Online ISBN: 978-3-540-49020-3
eBook Packages: Springer Book Archive