Dynamic Frames in Java Dynamic Logic: Formalisation and Proofs

Technical Report

Author(s):Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß
Institution:Department of Computer Science, Karlsruhe Institute of Technology
Number:2010-11
Year:2010
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000018332
Links:

Abstract

In this paper we present a realisation of the concept of dynamic frames in a dynamic logic for verifying Java programs. This is achieved by treating sets of heap locations as first class citizens in the logic. Syntax and formal semantics of the logic are presented, along with sound proof rules for modularly reasoning about method calls and heap dependent symbols using specification contracts. This technical report accompagnies the paper published in the proceedings FoVeOOS 2010 and contains formalisations and proofs.

BibTeX

@TECHREPORT{SchmittEtAl2010,
  author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
  title = {Dynamic Frames in {Java} Dynamic Logic: Formalisation and Proofs},
  institution = {Department of Computer Science, Karlsruhe Institute of Technology},
  year = {2010},
  month = nov,
  number = {2010-11},
  abstract = {In this paper we present a realisation of the concept of dynamic frames
	in a dynamic logic for verifying Java programs. This is achieved
	by treating sets of heap locations as first class citizens in the
	logic. Syntax and formal semantics of the logic are presented, along
	with sound proof rules for modularly reasoning about method calls
	and heap dependent symbols using specification contracts. This technical
	report accompagnies the paper published in the proceedings FoVeOOS
	2010 and contains formalisations and proofs.},
  url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000018332}
}