Advertisement

Analysis of the equality relations for the program terms

  • P. G. Emelianov
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)

Abstract

In this article an abstract interpretation and formal language based analysis for imperative programs is presented. This analysis makes a lower approximation of the equality relations for the program terms, i.e. for a given program point our analysis produces a set of equalities t1=t2 where t1 and t2 represent program expressions such that their values are equal for any behavior of the program if this program point is reached. The results of the analysis can be used for debugging, verification, optimization and specialization of programs. An abstract semantics of Pascal-like language is described and some examples of the analysis are given.

Keywords

Semantic Property Abstract Interpretation Entry State Program Point Term Equality 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AU 72]
    A.Aho, J.Ullman. The theory of parsing, translation and compilation. Vol.1-Prentice-Hall Inc., Englewood Cliffs, NJ, 1972.Google Scholar
  2. [AWZ 88]
    B.Alpern, M.N.Wegman, F.K.Zadeck. Detecting equality of variables in programs.-Proc. of the 15 th Annual ACM Symposium Principles of Programming Languages, San Diego, USA, 1988. CA. ACM Press, New York, USA, pages 1–11, 1988.Google Scholar
  3. [Bou 93]
    F.Bourdoncle. Efficient chaotic iteration strategies with widenings.-Proc. of the International Conference Formal Methods in Programming and Their Applications, Novosibirsk, Russia, 1993. LNCS 735, Springer-Verlag, Berlin, Germany, pages 129–141, 1993.Google Scholar
  4. [BJ 92]
    M.Bruynooghe, G.Janssens. On abstracting the procedural behaviour of logic program.-Proc. of the First and Second Russian Conferences on Logic Programming, Irkutsk (1990) and St.Petersburg (1991), Russia. LNAI 592, Springer-Verlag, Berlin, Germany, pages 240–262, 1992.Google Scholar
  5. [CCH 95]
    A.Cortesi,B.Le Charlier,P.Van Hentenryck. Type analysis of Prolog using type graphs.-Journal of Logic Programming, 16(2), pages 179–209, 1995.Google Scholar
  6. [CC 77]
    P.Cousot, R.Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints.-Proc. of the 4 th Annual ACM Symposium Principles of Programming Languages, Los-Angeles, USA, 1977. CA. ACM Press, New York, USA, pages 238–252, 1977.Google Scholar
  7. [CC 79]
    Cousot P., Cousot R. Systematic design of program analysis frameworks.-Rec. of the 6 th ACM Symposium on Principles of Programming Languages, San Antonio, USA, 1979. TX. ACM Press, New York, USA, pages 269–282, 1979.Google Scholar
  8. [CC 92a]
    P.Cousot, R.Cousot. Abstract interpretation frameworks.-Journal of Logic and Computation, 2(4), pages 511–547, 1992.Google Scholar
  9. [CC 92b]
    P.Cousot, R.Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper.-Proc. of the 5 th International Symposium Programming Language Implementation and Logic Programming, Leuven, Belgium, 1992. LNCS 631, Springer-Verlag, Berlin, Germany, pages 269–295, 1992.Google Scholar
  10. [CC 95]
    P.Cousot, R.Cousot. Formal languages, grammar and set-constraint-based program analysis by abstract interpretation.-Rec. of the Functional Programming Languages and Computer Architecture SIGPLAN-SIGARCH-WG 2.8, La Jolla, USA, 1995. CA. ACM Press, New York, USA, pages 170–181, 1995.Google Scholar
  11. [Deu 92]
    A.Deutsch. A storeless model of aliasing and its abstraction using finite representation of right-regular equivalence relations.-Proc. of the IEEE International Conference on Compiler Languages, pages 2–13, 1992.Google Scholar
  12. [Deu 94]
    A.Deutsch. Interprocedural may-alias analysis for pointers: beyond k-limiting.-Proc. of the ACM SIGPLAN'94 Conference on Program Language Design and Implementation, SIGPLAN Notices, 29(6), pages 230–241, 1994.Google Scholar
  13. [ELS 93]
    P.Eades, X.Lin, W.F.Smyth. A fast and effective heuristic for the feedback arc set problem.-Information Processing Letters, 47(6), pages 319–323, 1993.Google Scholar
  14. [ES 94]
    P.Emelianov, V.Sabelfeld. Analyzer of semantic properties of Modula-programs.-Software intellectualization and quality, Novosibirsk, Russia, pages 13–21, 1994, in russian.Google Scholar
  15. [GJ 79]
    M.R.Garey, D.S.Johnson. Computers and intractability. A guide to the theory of {ie188-01}-completeness.-W.H.Freeman and company, New York, USA, 1979.Google Scholar
  16. [Jo 87]
    N.D.Jones. Flow analysis of lazy higher-order functional programs.-In Abstract Interpretation of Declarative Languages, (Eds.: S.Abramsky and C.Hankin), Ellis Horwood, Chichester, UK, pages 103–122, 1987.Google Scholar
  17. [Hei 92]
    N.Heintze. Set based program analysis.-Ph.D. Thesis, School of Computer Sciences, Carnegie Mellon University, Pittsburg, USA, 1992.Google Scholar
  18. [Mas 93]
    F.Masdupuy. Semantic analysis of interval congruences.-Proc. of the International Conference Formal Methods in Programming and Their Applications, Novosibirsk, Russia, 1993. LNCS 735, Springer-Verlag, Berlin, Germany, pages 142–155, 1993.Google Scholar
  19. [NO 80]
    G.Nelson, D.C.Oppen. Fast decision procedures based on congruence closure.-Journal of the ACM, 27(2), pages 356–364, 1980.Google Scholar
  20. [Sa 80]
    V.Sabelfeld. The logic-termal equivalence is polynomial-time decidable.-Information Processing Letters, 10(2), pages 102–112, 1980.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • P. G. Emelianov
    • 1
  1. 1.Institute of Informatics SystemsNovosibirskRussia

Personalised recommendations