Conditional Effects in Fine-grained Region Logic
				  by
	     Yuyan Bao, Gary T. Leavens, and Gidon Ernst

			       Abstract

Specification languages have long featured ways to describe what does
not change when an imperative procedure is executed: the so-called
frame problem.  Solutions to the frame problem are needed for formal
verification in imperative programming, as otherwise a verification
would not be able to accumulate information from one statement to the
next.  Region logic is one of the approaches to solving the frame
problem.  We present a modified version of region logic with
fine-granularity and introduce conditional effects that allows one to
specify more precise frame conditions.

General terms: Verification

Keywords: Frame axiom, modifies clause, separation logic, dynamic
frames, region logic, formal methods, Dafny language, DafnyR language.

2013 CR Categories: 
D.2.4 [Software Engineering] Software/Program Verification — 
Formal methods, programming by contract; 
F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and
Reasoning about Programs — 
Assertions, logics of programs, pre- and post-conditions,
specification techniques.