A Programming Logic for Sequential Java

In: D. Swierstraed., ESOP '99. LNCS, volume 1576, 1999

Authors

• Arnd Poetzsch-Heffter
• Peter Müller

Abstract

"A Hoare-style programming logic for the sequential kernel of Java is presented. It handles recursive methods, class and interface types, subtyping, inheritance, dynamic and static binding, aliasing via object references, and encapsulation. The logic is proved sound w.r.t. an SOS semantics by embedding both into higher-order logic. BibTeX"

Full Text

• PDF: esop99.pdf
• PS.GZ: esop99.ps.gz

BibTeX

@InProceedings{Poetzsch-Heffter.Mueller99programming, 
   author = {Arnd Poetzsch-Heffter and Peter Müller}
   title = {A Programming Logic for Sequential Java},
   booktitle = {ESOP '99},
   series = {LNCS},
   publisher = {Springer},
   year = {1999},
}