Homepage>Publikationen>PublikationsDetail

Using Data Groups to Specify and Check Side Effects

In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. volume 37, number 5, p. 246--257, June, 2002

Authors

K. Rustan M. Leino
Arnd Poetzsch-Heffter
Yunhong Zhou

Abstract

Reasoning precisely about the side effects of procedure calls is important to many program analyses. This paper introduces a technique for specifying and statically checking the side effects of methods in an object-oriented language. The technique uses data groups, which abstract over variables that are not in scope, and limits program behavior by two alias-confining restrictions, pivot uniqueness and owner exclusion. The technique is shown to achieve modular soundness and is simpler than previous attempts at solving this problem.

Full Text

PDF: pldi02.pdf
PS.GZ: pldi02.ps.gz

BibTeX

@InProceedings{Leino.Poetzsch-Heffter.EA02using, 
   author = {K. Rustan M. Leino and Arnd Poetzsch-Heffter and Yunhong Zhou}
   title = {Using Data Groups to Specify and Check Side Effects},
   booktitle = {Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation},
   number = {5},
   pages = {246--257},
   month = {June},
   year = {2002},
}

Einloggen