Programming and Computer Software

, Volume 31, Issue 1, pp 1–9 | Cite as

Symbolic method of verification of definite iterations over altered data structures

  • V. A. Nepomniaschy


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.


Operating System Artificial Intelligence Data Structure Software Engineer Application Domain 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Hoare, C.A.R. 1969An Axiomatic Basis for Computer ProgrammingCommun. ACM12576580Google Scholar
  2. 2.
    Nepomniaschy, V.A., Ryakin, O.M. 1988Prikladnye metody verifikatsii programmRadio i Svyaz’Moscow(Applied Methods of Program Verification)Google Scholar
  3. 3.
    Stark, J., Ireland, A. 1999Invariant Discovery via Failed Proof AttemptsLecture Notes in Computer Science (Proc. LOPSTR’98)SpringerBerlin271288Google Scholar
  4. 4.
    Mills, H.D. 1986Structured Programming: Retrospect and ProspectIEEE Software35867Google Scholar
  5. 5.
    Linger, R., Mills, H., Witt, B. 1979Structured ProgrammingAddison-WesleyReadingTranslated under the title Teoriya i praktika strukturnogo programmirovaniya, Moscow: Mir, 1982Google Scholar
  6. 6.
    Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D. 2001Dynamically Discovering Likely Program Invariants to Support Program EvolutionIEEE Trans. Software Eng.2799123Google Scholar
  7. 7.
    Whalen, M., Schumann, J., Fischer, B. 2002Synthesizing Certified CodeLecture Notes in Computer Science (Proc. FME 2002)SpringerBerlin431450Google Scholar
  8. 8.
    Necula, G.C., Proof-Carrying Code, Proc. 24th Annu. ACM Symp. on Principles of Programming Languages, ACM, 1997, pp. 106–119.Google Scholar
  9. 9.
    Abd-El-Hafiz, S.K., Basili, V.R. 1996A Knowledgebased Approach to the Analysis of LoopsIEEE Trans. Software Eng.22339360Google Scholar
  10. 10.
    Stavely, A.M. 1995Verifying Definite Iteration over Data StructuresIEEE Trans. Software Eng.21506514Google Scholar
  11. 11.
    Nepomniaschy, V.A., Elimination of Loop Invariants in Program Verification, Programmirovanie, 1985, no. 3, pp. 3–13.Google Scholar
  12. 12.
    Nepomniaschy, V.A., On Problem-Oriented Verification of Programs, Programmirovanie, 1986, no. 1, pp. 3–12.Google Scholar
  13. 13.
    Nepomniaschy, V.A. 1993Verification of Programs over ArraysSistemnaya informatikaNaukaNovosibirsk6898Google Scholar
  14. 14.
    Nepomniaschy, V.A., Verification of Definite Iterations over Data Structures, Kibernetika i Sistemnyi Analiz, 1999, no. 3, pp. 25–37.Google Scholar
  15. 15.
    Nepomniaschy, V.A. 1999Verification of Definite Iteration over Hierarchical Data StructuresLecture Notes in Comput. Science (Proc. FASE/ETAPS’99)SpringerBerlin176187Google Scholar
  16. 16.
    Nepomniaschy, V.A., Verification of Finite Iterations over Tuples of Data Structures, Programmirovanie, 2002, no. 1, pp. 1–10.Google Scholar
  17. 17.
    Luckham, D.C., Suzuki, N. 1979Verification of Array, Record, and Pointer Operations in PascalACM Trans. Programming Languages Systems1226244Google Scholar
  18. 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.Google Scholar
  19. 19.
    Bornat R. Proving Pointer Programs in Hoare Logic. Lecture Notes in Computer Science (Proc. MPC 2000), Berlin: Springer, vol. 1837, pp. 102–126.Google Scholar
  20. 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.Google Scholar

Copyright information

© MAIK “Nauka/Interperiodica” 2005

Authors and Affiliations

  • V. A. Nepomniaschy
    • 1
  1. 1.Ershov Institute of Informatics Systems, Siberian DivisionRussian Academy of SciencesNovosibirskRussia

Personalised recommendations