Skip to main content
SpringerLink
Log in

Symbolic method of verification of definite iterations over altered data structures

  • Published:
Programming and Computer Software Aims and scope Submit manuscript

Abstract

To extend the application domain of the symbolic verification method, definite iterations over altered data structures, which are found to reduce to standard finite iterations, are introduced. The suggested reduction is applicable to definite iterations over altered data structures that contain an exit statement by a condition depending on the variables modified by the loop body. The suggested generalization of the symbolic method makes it applicable to verifying programs over pointers. To illustrate the discussion, the verification of two programs designed for processing linear lists-searching for an element with reordering and elimination of zero elements—is described.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

REFERENCES

  1. C.A.R. Hoare (1969) ArticleTitleAn Axiomatic Basis for Computer Programming Commun. ACM 12 IssueID1 576–580

    Google Scholar 

  2. V.A. Nepomniaschy O.M. Ryakin (1988) Prikladnye metody verifikatsii programm Radio i Svyaz’ Moscow

    Google Scholar 

  3. J. Stark A. Ireland (1999) Invariant Discovery via Failed Proof Attempts Lecture Notes in Computer Science (Proc. LOPSTR’98) Springer Berlin 271–288

    Google Scholar 

  4. H.D. Mills (1986) ArticleTitleStructured Programming: Retrospect and Prospect IEEE Software 3 IssueID6 58–67

    Google Scholar 

  5. R. Linger H. Mills B. Witt (1979) Structured Programming Addison-Wesley Reading

    Google Scholar 

  6. M.D. Ernst J. Cockrell W.G. Griswold D. Notkin (2001) ArticleTitleDynamically Discovering Likely Program Invariants to Support Program Evolution IEEE Trans. Software Eng. 27 IssueID2 99–123

    Google Scholar 

  7. M. Whalen J. Schumann B. Fischer (2002) Synthesizing Certified Code Lecture Notes in Computer Science (Proc. FME 2002) Springer Berlin 431–450

    Google Scholar 

  8. Necula, G.C., Proof-Carrying Code, Proc. 24th Annu. ACM Symp. on Principles of Programming Languages, ACM, 1997, pp. 106–119.

  9. S.K. Abd-El-Hafiz V.R. Basili (1996) ArticleTitleA Knowledgebased Approach to the Analysis of Loops IEEE Trans. Software Eng. 22 IssueID5 339–360

    Google Scholar 

  10. A.M. Stavely (1995) ArticleTitleVerifying Definite Iteration over Data Structures IEEE Trans. Software Eng. 21 IssueID6 506–514

    Google Scholar 

  11. Nepomniaschy, V.A., Elimination of Loop Invariants in Program Verification, Programmirovanie, 1985, no. 3, pp. 3–13.

  12. Nepomniaschy, V.A., On Problem-Oriented Verification of Programs, Programmirovanie, 1986, no. 1, pp. 3–12.

  13. V.A. Nepomniaschy (1993) Verification of Programs over Arrays Sistemnaya informatika Nauka Novosibirsk 68–98

    Google Scholar 

  14. Nepomniaschy, V.A., Verification of Definite Iterations over Data Structures, Kibernetika i Sistemnyi Analiz, 1999, no. 3, pp. 25–37.

  15. V.A. Nepomniaschy (1999) Verification of Definite Iteration over Hierarchical Data Structures Lecture Notes in Comput. Science (Proc. FASE/ETAPS’99) Springer Berlin 176–187

    Google Scholar 

  16. Nepomniaschy, V.A., Verification of Finite Iterations over Tuples of Data Structures, Programmirovanie, 2002, no. 1, pp. 1–10.

  17. D.C. Luckham N. Suzuki (1979) ArticleTitleVerification of Array, Record, and Pointer Operations in Pascal ACM Trans. Programming Languages Systems 1 IssueID2 226–244

    Google Scholar 

  18. Reynolds, J.C., Reasoning about Shared Mutable Data Structure, Proc. of the Symp. in Celebration of the Work of C.A.R. Hoare, Oxford, 1999, pp. 1–22.

  19. Bornat R. Proving Pointer Programs in Hoare Logic. Lecture Notes in Computer Science (Proc. MPC 2000), Berlin: Springer, vol. 1837, pp. 102–126.

  20. O’Hearn, P., Reynolds, J., and Yang, H., Local Reasoning about Programs that Alter Data Structures, Lecture Notes in Computer Science (Proc. CSL 2001), Berlin: Springer, vol. 2142, pp.1–19.

Download references

Author information

Authors and Affiliations

  1. Ershov Institute of Informatics Systems, Siberian Division, Russian Academy of Sciences, pr. Akademika Lavrent’eva 6, 630090, Novosibirsk, Russia

    V. A. Nepomniaschy

Authors
  1. V. A. Nepomniaschy
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Translated from Programmirovanie, Vol. 31, No. 1, 2005.

Original Russian Text Copyright © 2005 by Nepomniaschy.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Nepomniaschy, V.A. Symbolic method of verification of definite iterations over altered data structures. Program Comput Soft 31, 1–9 (2005). https://doi.org/10.1007/s11086-005-0007-7

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11086-005-0007-7

Keywords

Search

Navigation