Implicit dynamic frames: Combining dynamic frames and separation logic (soundness proof)

The dynamic frames approach has proven to be a powerful formalism for specifying and verifying object-oriented programs. However, it requires writing and checking many frame annotations. In this paper, we propose a variant of the dynamic frames approach that eliminates the need to explicitly write and check frame annotations. In this paper, we improve upon the classical dynamic frames approach in two ways: (1) method contracts are more concise and (2) fewer proof obligations must be discharged by the verifier. We have proven soundness, implemented the approach in a verifier prototype and demonstrated its expressiveness by verifying several challenging examples from related work.nrpages: 59status: publishe