Dynamic Frames in Java Dynamic Logic
Dynamic Frames in Java Dynamic Logic
复制标题
Java动态逻辑中的动态框架
DOI：
10.1007/978-3-642-18070-5_10
复制
发表时间：
2010
影响因子：
1.1
通讯作者：
Benjamin Weiß
中科院分区：
文献类型：
--
作者：
P. Schmitt;Mattias Ulbrich;Benjamin Weiß
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.
